Technische Universität
             Darmstadt leanCoP Logo University of Oslo

Lean Connection-Based Theorem Proving


  What is leanCoP?  
Download
Documentation
ileanCoP
MleanCoP
Contact
Documentation

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.


nanoCoP

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)


leanCoP 2.0

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


leanCoP 1.0

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)


MleanCoP

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)

ileanCoP

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)

Jens Otten · Institutt for informatikk · University of Oslo · 11.11.2016