A Linear Logic Prover (llprover). This small program searches a cut-free proof of the given two-sided sequent of first-order linear logic. Of course, the proof search of linear logic is undecidable. Therefore, this program limits the number of contraction rules for each path of the proof at most three (this threshold value can be changed). Formulas including additives, exponentials, or quantifiers can not be converted to Proof-net. To format LaTeX output, you need two style files: proof.sty (by Makoto Tatsuta) and linear.sty (does not work on LaTeX2e).
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Chaudhuri, Kaustuv; Pfenning, Frank; Price, Greg: A logical characterization of forward and backward chaining in the inverse method (2008)
- Chaudhuri, Kaustuv; Pfenning, Frank; Price, Greg: A logical characterization of forward and backward chaining in the inverse method (2006)
- Chaudhuri, Kaustuv; Pfenning, Frank: A focusing inverse method theorem prover for first-order linear logic (2005)
- Hayashi, Susumu; Sumitomo, Ryosuke; Shii, Ken-ichiro: Towards the animation of proofs -- testing proofs by examples (2002)