|
|
The following papers about the automated theorem provers
nanoCoP,
leanCoP 2.0,
leanCoP 1.0,
MleanCoP, and
ileanCoP
contain details about the underlying connection calculi,
descriptions of the implementations and comprehensive
performance results.
The following paper provides details about the classical
non-clausal connection prover
nanoCoP.
-
nanoCoP: A Non-clausal Connection Prover.
Jens Otten.
In N. Olivetti, A. Tiwari, editors,
International Joint Conference on Automated Reasoning,
IJCAR 2016.
© Springer
Verlag, 2016.
nanocop_ijcar16.pdf
(207 kbytes)
-
A Non-clausal Connection Calculus.
Jens Otten.
In K. Brünnler and G. Metcalfe, editors,
Automated Reasoning with Analytic Tableaux and Related Methods,
TABLEAUX 2011, LNAI 6793, pages 226-241.
© Springer
Verlag, 2011.
concalc_tab11.pdf
(307 kbytes)
The following papers provide details about the classical connection
prover
leanCoP 2.0.
-
Restricting Backtracking in Connection Calculi.
Jens Otten.
AI Communications, volume 23, No. 2-3, pages 159-182.
© IOS Press,
2010.
restricting_backtracking_aicom10.pdf
(289 kbytes)
-
leanCoP 2.0 and ileanCoP 1.2: High Performance Lean
Theorem Proving in Classical and Intuitionistic Logic.
Jens Otten.
In A. Armando, P. Baumgartner, G. Dowek, editors, Automated
Reasoning, IJCAR 2008, LNAI 5195, pages 283-291.
© Springer
Verlag, 2008.
leancop20_ijcar08.pdf
(176 kbytes)
leancop20_ijcar08.dvi
(50 kbytes)
There is a short paper available about the classical connection
prover
leanCoP 1.0
as well as a more detailed journal article.
-
leanCoP: Lean Connection-Based Theorem Proving.
Jens Otten and Wolfgang Bibel.
Journal of Symbolic Computation, Volume 36, pages 139-161.
© Elsevier
Science, 2003.
leancop_jsc.pdf
(280 kbytes)
leancop_jsc.dvi
(94 kbytes)
-
leanCoP: Lean Connection-Based Theorem Proving.
Jens Otten and Wolfgang Bibel.
Third International Workshop on First-Order Theorem Proving.
Research Report 5/2000, pages 153-159,
Universität Koblenz-Landau, 2000.
leancop_ftp00.pdf
(173 kbytes)
leancop_ftp00.dvi
(28 kbytes)
The following papers provide details about version 1.2 and
version 1.3 of the first-order modal connection prover
MleanCoP.
-
MleanCoP: A Connection Prover for First-Order Modal
Logic.
Jens Otten.
In S. Demri, D. Kapur, C. Weidenbach, editors,
International Joint Conference on Automated Reasoning,
IJCAR 2014, LNAI 8562, pages 269-276.
© Springer
Verlag, 2014.
mleancop_ijcar14.pdf
(202 kbytes)
-
Implementing and Evaluating Provers for First-order
Modal Logics.
Christoph Benzmüller, Jens Otten, Thomas Raths.
In L. De Raedt et al., editors,
20th European Conference on Artificial Intelligence, ECAI 2012,
pages 163-168.
© IOS Press, 2012.
modal_ecai12.pdf
(295 kbytes)
-
Implementing Connection Calculi for First-order Modal
Logics.
Jens Otten.
In E. Ternovska, K. Korovin, S. Schulz, editors,
International Workshop on the Implementation of Logics (IWIL-2012),
Merida/Venezuela, 2012.
mleancop_iwil12.pdf
(302 kbytes)
mleancop_iwil12.dvi
(139 kbytes)
The following papers provide details about version 1.0
and version 1.2 of the intuitionistic connection prover
ileanCoP.
-
leanCoP 2.0 and ileanCoP 1.2: High Performance Lean
Theorem Proving in Classical and Intuitionistic Logic.
Jens Otten.
In A. Armando, P. Baumgartner, G. Dowek, editors, Automated
Reasoning, IJCAR 2008, LNAI 5195, pages 283-291.
© Springer
Verlag, 2008.
leancop20_ijcar08.pdf
(176 kbytes)
leancop20_ijcar08.dvi
(50 kbytes)
-
Clausal Connection-Based Theorem Proving in Intuitionistic
First-Order Logic.
Jens Otten.
In B. Beckert, editor, Automated Reasoning with Analytic Tableaux
and Related Methods, TABLEAUX 2005, LNAI 3702, pages 245-261.
© Springer
Verlag, 2005.
ileancop_tab05.pdf
(320 kbytes)
ileancop_tab05.dvi
(87 kbytes)
|