A Linear Logic Prover (llprover)
If you are looking for a sequent calculus prover for
firstorder classical logic (LK),
please check
Sequent Prover (seqprover).
What's New

Dec 30, 2020: GitPod for running llprover
 Dec 19, 2020:
Modified for SWI Prolog.
 Feb 26, 2000:
LaTeX output is modified for SICStus Prolog 3.7.1.
 May 29, 1998:
English documents are now available.
 Dec 19, 1997:
Some bugs are fixed.
 Sep 24, 1997:
llprover was demonstrated at TACS97.
 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.
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 Prolog program
is here (38KB).
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
Most of the links are broken...
 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