-
Notifications
You must be signed in to change notification settings - Fork 2
Home
Olivier Laurent edited this page Apr 28, 2021
·
53 revisions
- request to an automated prover
- add cut rule
- LaTeX export with implicit exchange rule (matching what is on the screen)
- explicit exchange rule (with colored backgrounds to follow instances of formulas) (issue #11)
- formula naming through (possibly recursive) equations (with click on name to unfold a definition inside a proof)
- two-sided sequent calculus
- intuitionistic linear logic
- quantifiers (issue #16)
- contexts as first-class objects (issue #13)
- cyclic linear logic (exchange restricted to circular shifts, requires to modify the definition of dual of a formula)
- additional tool for proof transformations (cut elimination, axiom expansion, reversing, focusing, substitution, etc.) (issue #12)
- back edges for regular proofs
- fixed-point connectives in formulas
- mix rules (note mix2 can be faithfully simulated by adding
?(⊥⊗⊥)in the context, and similarly for mix0 with?1) - export to proof-nets