A Linear Logic Prover (llprover)

If you are looking for a sequent calculus prover for first-order classical logic (LK), please check Sequent Prover (seqprover).

What's New


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.

Any comments or suggestions are appreciated.

System names, notations, and examples are based on Troelstra's text book: Lectures on Linear Logic, CSLI Lecture Notes No.29, 1992.


The prover Prolog program is here (38KB).


Known Bugs

Related Links

Most of the links are broken...
Linear Logic Provers/Proof Editors
Provers/Proof Editors on the Internet
Related Pages

Naoyuki Tamura