## linTAP: A Tableau Prover for Linear Logic What is linTAP? · Documentation · Source Code · Related Links · Contact Us Potsdam University Computer Science Theoretical CS
 What is linTAP?

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.

 Documentation

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)

 Source Code

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.