ileanTAP is a Prolog program that implements a sound and complete
theorem prover for first-order intuitionistic logic. It is based on
free-variable semantic tableaux extended by an additional prefix
unification to ensure the particular restrictions in intuitionistic
logic. Due to the modular treatment of the different connectives
the implementation can easily be adapted to deal with other
Features of ileanTAP
Theorem prover for intuitionistic first-order logic.
Based on a free-variable semantic tableau calculus.
Sound and complete.
Decision procedure for the fragment where negation
occurs only positively and which contains only existential
Source code available for popular
Prolog systems, including ECLiPSe Prolog, SWI-Prolog and
Simple first-order form input format.
The short paper contains a description of the
source code and some performance results achieved with ileanTAP.
ileanTAP: An Intuitionistic Theorem Prover.
In D. Galmiche, editor, International Conference TABLEAUX'97,
LNAI 1227, pages 307-312.
Springer Verlag, 1997.
The source code of ileanTAP is available for
it should run on most other Prolog systems as well.
Please contact us if you encounter
any problems when downloading or running ileanTAP on your system.
The ileanTAP prover is invoked with
prove(F). where F
is a first-order formula. For example
prove( all X: ex Y:(~q,p(Y) => p(X)) ).
will prove the validity of the given formula.
The logical connectives are expressed by "~" (negation),
"," (conjunction), ";" (disjunction), "=>"
(implication), "<=>" (equivalence); quantifiers are
expressed by "all X:" (universal) and "ex X:"
(existential). See the
documentation for more details about
the syntax of first-order formulas.
Here is a selection of links related to ileanTAP.
- a compact Prolog theorem prover for first-order logic based on
analytic tableaux by Bernhard Beckert and Joachim Posegga.
- a compact Prolog theorem prover for modal logics based on
analytic tableaux by Bernhard Beckert and Rajeev Goré.
- a compact Prolog theorem prover for the multiplicative and
exponential fragment of Girard's linear logic.
- a compact Prolog theorem prover for classical-first order
- a compact Prolog non-clausal "Davis-Putnam" prover.
Please feel free to contact us if you have any
questions about ileanTAP. If you have any suggestions for improvements
or if you have done something interesting with ileanTAP, please
let us know about it.