LinearOne
LinearOne copied to clipboard
RichardMoot
LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.
Currently, the proof output produces long normal form proofs (ie. beta-normal eta-long proofs). This makes sense from the point of view of proof search, but can be more user-friendly to...
Forall links have the property that no atom containing the eigenvariable of a link can every be identified with a node which dominates the forall link of this variable. Adding...
Add additives together with a contraction condition as proposed by Maieli. This will be a major update/rewrite since it will complicate (at least) the axiom linking component: it will allow...
Metadata
Owner
Metadata
LinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.