A Linear Logic Prover (llprover)

Last modified: Wed May 9 16:39:04 2007 JST

  1. Please select a system:
  2. Please input a sequent:
    or select an example:
    See more examples. See documents for the syntax.
  3. Please select a output style:
  4. Please limit the number of contraction rules for each path:
  5. Now, press or
    Process spending more than 120 seconds will be killed.
  6. Example outputs are here and here and here and here.
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 (does not work on LaTeX2e).

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 program (written in SICStus Prolog 2.1) is here (38KB). The whole package is llprover1.4.tar.gz (CGI program is not included). Here is statistics information.


Known Bugs

Related Links

Linear Logic Provers/Proof Editors
Provers/Proof Editors on the Internet
Related Pages

Naoyuki Tamura / Dept of CS / Kobe University / Japan
This page has been accessed ????? times since Jan 1, 1999.