A Linear Logic Prover (llprover)
Last modified: Wed May 9 16:39:04 2007 JST
If you are looking for a sequent calculus prover for
firstorder 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 redisplayed 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 milliseconds)
 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 cutfree proof of the given
twosided sequent of firstorder
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 Proofnet.
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
(PDF)
 User's guide in Japanese
(PDF)
Known Bugs
 Occur check is not included.
 Do not use free variables (e.g. a(X) > a(1)).
Related Links
 Linear Logic Provers/Proof Editors


Rits Concurrency Workbench
(Java applet,
Japanese page is also available)
This Java applet helps you to write/edit a proofnet and
to translate it to a sequent or
a picalculus expression.
Satoshi Akazawa and
Yukihide Takayama, Ritsumeikan University, Japan
 Linprove (Linseq & Linres)
(C program)
Tanel Tammet,
Chalmers University of Technology, Sweden

MALL prover
(Prolog program)
Natarajan Shankar,
Computer Science Laboratory, SRI
 Linear Logic prover in Isabelle
Sara Kalvala and
Jane Sinclair,
Department of Computer Science,
University of Warwick, UK

Xpnet: A Graphical Interface to Proof Nets
with an Efficient Proof Checker
Jawahar Chirimar,
Carl A. Gunter,
and Myra VanInwegen,
Dept. of Computer and Information Science,
University of Pennsylvania, USA

Linear Logic Proof Game (Java Applet)
Advait Deodha, Cory Meek, and
Andre Scedrov,
Department of Mathematics,
University of Pennsylvania, USA

linTAP: A Tableau Prover for Linear Logic
(Prolog program)
Jens Otten,
Fachbereich Informatik
Darmstadt University of Technology, Germany
 Provers/Proof Editors on the Internet

 Sequent Prover (seqprover) (CGI)

Gateway to Logic (Java Applet)
Christian Gottschall,
Department of Philosopy, University of Vienna, Austria

Logic Daemon (CGI)
Colin Allen
and Song Chen,
Texas A&M University, USA

Interactive ProofCheckers (Java Applet)
Peter Gibbins, ,Oxford Virtual Technology, UK

Metamath Solitaire (Java Applet)
Norman Megill, USA

Internet Prover *SKIP*
(Java applet)
Daisuke Nagono and
Sachio Hirokawa, Kyushu University, Japan

An Implementation of G4ip in Pizza
(Java applet)
Chiristian Urban,
Computer Laboratory, University of Cambridge, UK

Pier, Proof Interactive Editor
(Java applet)
Masaru Shirahata, Keio University, Japan

PProver & JProver
(CGI & Java applet,
Japanese page is also available)
Kakehi Laboratory, Waseda University, Japan

Logics Workbench
(CGI)
the University of Berne, Switzerland

The Carnegie Mellon Proof Tutor
(telnet)

SCAN
(CGI)

xpe: X window system Proof Editor (for LaTeX proof.sty)
Motohiko Mouri, JAIST, Japan
 Related Pages

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