The ILTP Library

Benchmarking Theorem Provers for Intuitionistic Logic


Welcome
Benchmark Problems
Provers and Results
Contact
 
Provers and Results

The following is a list of automated theorem proving systems for intuitionistic logic. For each system the following information is provided: name, version, author, homepage/download address, a short description with details about the used algorithm/calculus and programming language, example sessions, references, performance results on the benchmark problems in the ILTP library, and the format file. The format file is used in conjuction with the tptp2X tool for converting problems from the ILTP/TPTP syntax into the input syntax of an ATP systems. All format files are already included in the downloadable problem collections of the ILTP library. The readme file contains more information on how to use the tptp2X tool.

The following files contain overall statistics and performance comparisons of first-order and propositional intuitionistic ATP systems on all problems in the ILTP library:

The list below contains information about the following intuitionistic ATP systems:

It is likely that this list is incomplete. We appreciate any information about intuitionistic ATP systems you would like to see included in this list. If you have tested your system on the benchmark problems in the ILTP library we would like to hear about it. Please contact us so that we can update the information in this list.


ft-C

Name/version: ft version 1.23 (C)
Author(s): D. Sahlin, T. Franzen, S. Haridi (Swedish Institute of Computer Science)
Homepage/download: http://www.sics.se/isl/ft.html
http://www.sm.luth.se/ ~torkel/ eget/ ftinfo.html
Description: Analytic tableau prover for first-order logic using many optimization techniques implemented in C. Decides propositional logic by using a contraction-free calculus.
Examples: ft-C_example.txt (1 kbyte)
References: D. Sahlin, T. Franzen, S. Haridi. An Intuitionistic Predicate Logic Theorem Prover. Journal of Logic and Computation, 2(5):619-656, 1992.
Performance results: 2550 problems (ILTP v1.1.2-fof)
  364 solved (14%)
  (334 proved, 30 refuted)
274 problems (ILTP v1.1.2-prop)
  199 solved (73%)
  (106 proved, 93 refuted)
Detailed results: ft-C_on_ILTP-v1.1.2-fof.txt (84 kbytes)
ft-C_on_ILTP-v1.1.2-prop.txt (9 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, gcc version 3.3.1
Format file: format.ft (8 kbytes)

ft-Prolog

Name/version: ft version 1.23 (Prolog)
Author(s): D. Sahlin, T. Franzen, S. Haridi (Swedish Institute of Computer Science)
Homepage/download: http://www.sm.luth.se/ ~torkel/ eget/ ftinfo.html http://www.sics.se/isl/ft.html
Description: Analytic tableau prover for first-order logic using many optimization techniques implemented in Prolog. Decides propositional logic by using a contraction-free calculus.
Examples: ft-Prolog_example.txt (2 kbytes)
References: D. Sahlin, T. Franzen, S. Haridi. An Intuitionistic Predicate Logic Theorem Prover. Journal of Logic and Computation, 2(5):619-656, 1992.
Performance results: 2550 problems (ILTP v1.1.2-fof)
  299 solved (12%)
  (299 proved, 0 refuted)
274 problems (ILTP v1.1.2-prop)
  188 solved (69%)
  (104 proved, 84 refuted)
Detailed results: ft-Prolog_on_ILTP-v1.1.2-fof.txt (84 kbytes)
ft-Prolog_on_ILTP-v1.1.2-prop.txt (9 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, ECLiPSe v5.8 #70 (using ECLiPSe flag "nodbgcomp.")
Format file: format.ftprolog (7 kbytes)

Gandalf

Name/version: Gandalf version 0.2 (intuitionistic version)
Author(s): T. Tammet (Tallinn Technical University)
Homepage/download: http://deepthought.ttu.ee/it/gandalf
Description: Resolution prover for first-order logic implemented in Scheme and compiled to C.
Examples: Gandalf_example.txt (4 kbytes)
References: T. Tammet. A Resolution Theorem Prover for Intuitionistic Logic. CADE-13, LNCS 1104, pages 2-16, Springer, 1996.
Performance results: (Prover seems to be incorrect.)
Detailed results: Gandalf_on_ILTP-v1.1.1-fof.txt (97 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, gcc version 3.4.3
Format file: format.gandalf (8 kbytes)

JProver

Name/version: JProver (MetaPRL version 0.9.6.4+, MetaPRL-SVN-2005.11.27)
Author(s): S. Schmitt, A. Nogin (CalTech), Y. Bryukhov (CUNY)
Homepage/download: http://cvs.metaprl.org:12000/ metaprl/ default.html (JProver is included in the MetaPRL distribution; see also this JProver readme file)
Description: Non-clausal connection calculus for first-order logic using prefix unification implemented in OCaml. Decides some propositional and first-order problems.
Examples: JProver_example.txt (1 kbyte)
References: S. Schmitt et al. JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants. IJCAR-2001, LNAI 2083, pages 421-426, Springer, 2001.
Performance results: 2550 problems (ILTP v1.1.2-fof)
  268 solved (11%)
  (264 proved, 4 refuted)
Detailed results: JProver_on_ILTP-v1.1.2-fof.txt (84 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, OCaml v3.09, Omake 0.9.6
Format file: format.jprover (7 kbytes)

LJT

Name/version: LJT version 1.0
Author(s): R. Dyckhoff (University of St Andrews)
Homepage/download: http://www.dcs.st-and.ac.uk/ ~rd/ logic/ nonmac/ LJT.pl.html
Description: Contraction-free (analytic) sequent calculus for propositional logic implemented in Prolog. Decision procedure for propositional problems.
Examples: LJT_example.txt (1 kbyte)
References: R. Dyckhoff. Contraction-free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic, 57:795-807, 1992.
Performance results: 274 problems (ILTP v1.1.2-prop)
  175 solved (64%)
  (108 proved, 67 refuted)
Detailed results: LJT_on_ILTP-v1.1.2-prop.txt (9 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, ECLiPSe v5.8 #70 (using ECLiPSe flag "nodbgcomp.")
Format file: format.ljt (6 kbytes)

PITP

Name/version: PITP version 3.0
Author(s): A. Avellone, G. Fiorino, U. Moscato (University of Milano-Bicocca)
Homepage/download: http://www.dimequant.unimib.it/ PITP/
Description: Duplication-free tableau calculus for propositional logic implemented in C++. Decision procedure for propositional problems.
Examples: PITP_example.txt (1 kbyte)
References: A. Avellone, G. Fiorino, U. Moscato. A New o(n log n)-Space Decision Procedure for Propositional Intuitionistic Logic. Kurt Goedel Society Collegium Logicum, volume VIII, pages 17-33, 2004.
Performance results: 274 problems (ILTP v1.1.2-prop)
  238 solved (87%)
  (128 proved, 110 refuted)
Detailed results: PITP_on_ILTP-v1.1.2-prop.txt (10 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, gcc version 3.4.3
Format file: format.pitp (7 kbytes)

PITPINV

Name/version: PITPINV
Author(s): A. Avellone, G. Fiorino, U. Moscato (University of Milano-Bicocca)
Homepage/download: http://www.dimequant.unimib.it/ PITP/
Description: Duplication-free tableau calculus for propositional logic implemented in C++. Decision procedure for propositional problems. Implements the same FT search strategy, namely for the semi invertible rules the non invertible branch is the first to be visited.
Examples: PITP_example.txt (1 kbyte)
References: A. Avellone, G. Fiorino, U. Moscato. A New o(n log n)-Space Decision Procedure for Propositional Intuitionistic Logic. Kurt Goedel Society Collegium Logicum, volume VIII, pages 17-33, 2004.
Performance results: 274 problems (ILTP v1.1.2-prop)
  262 solved (96%)
  (128 proved, 134 refuted)
Detailed results: PITPINV_on_ILTP-v1.1.2-prop.txt (10 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, gcc version 3.4.3
Format file: format.pitp (7 kbytes)

IPTP

Name/version: IPTP version 1.0
Author(s): A. Avellone, G. Fiorino, U. Moscato (University of Milano-Bicocca)
Homepage/download: http://www.dimequant.unimib.it/ IPTP/
Description: Parallel version of a duplication-free tableau calculus for propositional logic implemented in C++. Decision procedure for propositional problems.
Examples: IPTP_example.txt (1 kbyte)
References: A. Avellone, G. Fiorino, U. Moscato. A Parallel Implementation of a Decision Procedure for Propositional Intuitionistic Logic. TABLEAUX 2003 (Position Papers and Tutorials), Technical Report RT-DIA-80-2003, Dipartimento di Informatica e Automazione, Universit´┐Ż degli Studi di Roma 3, pages 14-22, 2003.
Performance results: 274 problems (ILTP v1.1.1-prop)
  209 solved (76%)
  (127 proved, 82 refuted)
Detailed results: IPTP_on_ILTP-v1.1.1-prop.txt (10 kbytes)
Test platform: HP SD64000, PA-8700 750MHz, HP-UX 11i
Format file: format.pitp (7 kbytes)

STRIP

Name/version: STRIP version 1.1
Author(s): Dominique Larchey, Daniel Mery and Didier Galmiche (LORIA)
Homepage/download: http://www.loria.fr/ ~larchey/ STRIP/
Description: Contraction-free (analytic) sequent calculus for propositional logic implemented in C. Decision procedure for propositional formulas.
Examples: STRIP_example.txt (1 kbyte)
References: D. Larchey-Wendling, D. Méry, D. Galmiche. STRIP: Structural Sharing for Efficient Proof-Search. IJCAR-2001, LNAI 2083, pages 696-700, Springer, 2001.
Performance results: 274 problems (ILTP v1.1.2-prop)
  205 solved (75%)
  (120 proved, 85 refuted)
Detailed results: STRIP1.1_on_ILTP-v1.1.2-prop.txt (9 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2
Format file: format.strip (7 kbytes)

ileanCoP

Name/version: ileanCoP version 1.0
Author(s): J. Otten (University of Potsdam)
Homepage/download: http://www.leancop.de/ ileancop
Description: Clausal connection calculus for first-order logic using prefix unification implemented in Prolog. Decides some propositional and first-order formulas.
Examples: ileanCoP_example.txt (1 kbyte)
References: J. Otten. Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic. Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2005, LNAI 3702, pages 245-261, Springer, 2005.
Performance results: 2550 problems (ILTP v1.1.2-fof)
  690 solved (27%)
  (610 proved, 80 refuted)
Detailed results: ileanCoP_on_ILTP-v1.1.2-fof.txt (84 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, ECLiPSe v5.8 #70 (using ECLiPSe flag "nodbgcomp.")
Format file: format.leancop (8 kbytes)

ileanTAP

Name/version: ileanTAP version 1.17
Author(s): J. Otten (University of Potsdam)
Homepage/download: http://www.leancop.de/ ileantap
Description: Analytic tableau prover for first-order logic using prefix unification implemented in Prolog. Decides some propositional and first-order formulas.
Examples: ileanTAP_example.txt (1 kbyte)
References: Jens Otten. ileanTAP: An Intuitionistic Theorem Prover. International Conference TABLEAUX '97, LNAI 1227, pages 307-312. Springer, 1997.
Performance results: 2550 problems (ILTP v1.1.2-fof)
  315 solved (12%)
  (311 proved, 4 refuted)
Detailed results: ileanTAP_on_ILTP-v1.1.2-fof.txt (84 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, ECLiPSe v5.8 #70 (using ECLiPSe flag "nodbgcomp.")
Format file: format.leancop (8 kbytes)

ileanSeP

Name/version: ileanSeP version 1.0
Author(s): J. Otten (University of Potsdam)
Homepage/download: http://www.leancop.de/ ileansep
Description: Analytic sequent calculus with free variables (tableau-like) for first-order logic implemented in Prolog. Decides some propositional and first-order formulas.
Examples: ileanSeP_example.txt (1 kbyte)
References: http://www.leancop.de/ileansep
Performance results: 2550 problems (ILTP v1.1.2-fof)
  313 solved (12%)
  (309 proved, 4 refuted)
Detailed results: ileanSeP_on_ILTP-v1.1.2-fof.txt (76 kbytes)
Test platform: Xeon 3.4 GHz, Mandrake 10.2, ECLiPSe v5.8 #70 (using ECLiPSe flag "nodbgcomp.")
Format file: format.leancop (8 kbytes)


Jens Otten / Thomas Raths 01.03.2007