|
|
|
|
linTAP is a tableau prover for the multiplicative and exponential
fragment of Girards linear logic. It proves the classical validity
of a given formula by constructing an analytic tableau and ensures
the linear validity using prefix unification. Due to the compact code
the program can easily be modified for special purposes or applications.
Features of linTAP
-
Theorem prover for the multiplicative, exponential fragment M?LL of
linear logic.
-
Based on a prefixed semantic tableau calculus.
-
Sound and complete.
-
Source code available for popular
Prolog systems, including ECLiPSe Prolog, SWI-Prolog and
SICStus Prolog.
-
Simple input format.
The following paper provides a description of
the prefixed tableau calculus and the source code. Some
performance results are presented as well.
-
Heiko Mantel and Jens Otten.
linTAP: A Tableau Prover for Linear Logic.
In N. Murray, editor, International Conference TABLEAUX'99.
LNAI 1617, pages 217-231, Springer Verlag, 1999.
·
lintap_tab99.pdf
(327 kbytes)
·
lintap_tab99.dvi
(141 kbytes)
The source code of linTAP is available for
ECLiPSe Prolog,
SWI-Prolog and
SICStus Prolog;
it should run on most other Prolog systems as well.
Please contact us if you encounter
any problems when downloading or running linTAP on your system.
The linTAP prover is invoked with
prove(F). where F
is a formula in linear logic. For example
prove( (((a@0)*a)@ ?(~a)) ).
will prove the validity of the given formula.
The logical connectives are expressed by "~" (negation),
"*" (conjunction), "@" (disjunction), "@>"
(implication); exponentials are expressed by "?" and "!",
the constants by "1" and "0". See the
documentation for more details about
the syntax of formulas in linear logic.
Here is a selection of interesting links related to linTAP.
-
leanTAP
- a compact Prolog theorem prover for first-order logic based on
analytic tableaux by Bernhard Beckert and Joachim Posegga.
-
ModLeanTAP
- a compact Prolog theorem prover for modal logics based on
analytic tableaux by Bernhard Beckert and Rajeev Goré.
-
ileanTAP
- a compact Prolog theorem prover for intuitionistic
first-order logic based on analytic tableaux and
prefix unification.
-
leanCoP
- a compact Prolog theorem prover for classical-first order
logic.
-
ncDP
- a compact Prolog non-clausal "Davis-Putnam" prover.
Please feel free to contact us if you have any
questions about linTAP. If you have any suggestions for improvements
or if you have done something interesting with linTAP, please
let us know about it.
|
