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
-
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 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.
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 proof-net and
to translate it to a sequent or
a pi-calculus 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 Proof-Checkers (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
-
P-Prover & 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