The following papers about the automated theorem provers leanCoP 2.0, leanCoP 1.0 and ileanCoP contain details about the underlying connection calculi, descriptions of the implementations and comprehensive performance results.

The following papers provide details about the classical connection prover leanCoP 2.0.

• Jens Otten.
  Restricting Backtracking in Connection Calculi.
  AI Communications. © IOS Press, 2010. To appear.

  restricting_backtracking_aicom10.pdf (289 kbytes)

• Jens Otten.
  leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic.
  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.

• Jens Otten and Wolfgang Bibel.
  leanCoP: Lean Connection-Based Theorem Proving.
  Journal of Symbolic Computation, Volume 36, pages 139-161. © Elsevier Science, 2003.

  leancop_jsc.pdf (280 kbytes)
  leancop_jsc.dvi (94 kbytes)

• Jens Otten and Wolfgang Bibel.
  leanCoP: Lean Connection-Based Theorem Proving.
  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.0 and version 1.2 of the intuitionistic connection prover ileanCoP.

• Jens Otten.
  leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic.
  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)

• Jens Otten.
  Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic.
  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)