A Linear Logic Prover (llprover)

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

Please select a system:
Please input a sequent:
or select an example:
See more examples. See documents for the syntax.
Please select a output style:
Please limit the number of contraction rules for each path:
Now, press or
Process spending more than 120 seconds will be killed.
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

Feb 26, 2000: LaTeX output is modified for SICStus Prolog 3.7.1.
May 29, 1998: English documents are now available.
May 25, 1998: Input form is re-displayed in the result page.
May 6, 1998: Now, you can use formulas for input (e.g. a+b->b+a). In the previous version, you need to write it as [] --> a+b->b+a.
Dec 19, 1997: Some bugs are fixed. Please try
!all(X,n(X)->n(s(X))),!n(0) --> n(s(s(0))) (CPU time is about 220 milli-seconds)
Nov 18, 1997: Statistics is added.
Sep 24, 1997: llprover was demonstrated at TACS'97.
Sep 3, 1997: More examples are added.
Sep 3, 1997: <--> proves in both directions.
May 8, 1997: Variables will be named like X, Y, Z, ... in pretty output form.
May 8, 1997: I fixed a bug in quantifier rules.

Introduction

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.

Program

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.

Documents

User's guide in English (PostScript, DVI)
User's guide in Japanese (PostScript, DVI)

Known Bugs

Occur check is not included.
Do not use free variables (e.g. a(X) --> a(1)).