|
|
|
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:
-
First-order ATP systems:
ft-C,
ft-Prolog,
Gandalf,
JProver,
ileanCoP,
ileanTAP,
ileanSeP.
-
Propositional ATP systems:
ft-C,
ft-Prolog,
LJT,
PITP,
PITPINV,
IPTP,
STRIP.
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.
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|
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)
|
|