ileanTAP: An Intuitionistic Theorem Prover

Universität Potsdam

What is ileanTAP?
 · Documentation
 · Source Code
 · Related Links
 · Contact Us
 
 
 
Potsdam University
Computer Science
Theoretical CS
What is ileanTAP?

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 non-classical logics.

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 quantified variables.
  • Source code available for popular Prolog systems, including ECLiPSe Prolog, SWI-Prolog and SICStus Prolog.
  • Simple first-order form input format.

Documentation

The short paper contains a description of the source code and some performance results achieved with ileanTAP.

  • Jens Otten.
    ileanTAP: An Intuitionistic Theorem Prover.
    In D. Galmiche, editor, International Conference TABLEAUX'97, LNAI 1227, pages 307-312.
    Springer Verlag, 1997.

      · ileantap_tab97.pdf (171 kbytes)
      · ileantap_tab97.dvi (31 kbytes)

Source Code

The source code of ileanTAP 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 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.


Related Links

Here is a selection of links related to ileanTAP.

  • 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é.
  • linTAP - a compact Prolog theorem prover for the multiplicative and exponential fragment of Girard's linear logic.
  • leanCoP - a compact Prolog theorem prover for classical-first order logic.
  • ncDP - a compact Prolog non-clausal "Davis-Putnam" prover.

Contact Us

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.


Jens Otten · Institut für Informatik · University of Potsdam · 03.03.2008