leanCoP

leanCoP is a very compact theorem prover for classical first-order logic, based on the connection (tableau) calculus and implemented in Prolog. leanCoP 2.0 enhances leanCoP 1.0 by adding regularity, lemmata, and a technique for restricting backtracking. It also provides a definitional translation into clausal form and integrates “Prolog technology” into a lean theorem prover. ileanCoP is a compact theorem prover for intuitionistic first-order logic and based on the clausal connection calculus for intuitionistic logic. leanCoP 2.0 extends the classical prover leanCoP 2.0 by adding prefixes and a prefix unification algorithm. We present details of both implementations and evaluate their performance.


References in zbMATH (referenced in 16 articles , 1 standard article )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
  2. Gilbert, Frédéric: Automated constructivization of proofs (2017)
  3. Färber, Michael; Brown, Chad: Internal guidance for Satallax (2016)
  4. Freitas, Fred; Otten, Jens: A connection calculus for the description logic $ \mathcalALC $ (2016)
  5. Otten, Jens: Nanocop: a non-clausal connection prover (2016)
  6. Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
  7. Otten, Jens: MleanCoP: a connection prover for first-order modal logic (2014)
  8. Alonderis, R.: A proof-search procedure for intuitionistic propositional logic (2013)
  9. Benzmüller, Christoph; Raths, Thomas: HOL based first-order modal logic provers (2013)
  10. Otten, Jens: A non-clausal connection calculus (2011)
  11. Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr: MaLeCoP. Machine learning connection prover (2011)
  12. Brandt, Christoph; Otten, Jens; Kreitz, Christoph; Bibel, Wolfgang: Specifying and verifying organizational security properties in first-order logic (2010)
  13. Otten, Jens: Restricting backtracking in connection calculi (2010)
  14. Otten, Jens: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic. (System descriptions) (2008)
  15. Otten, Jens: Clausal connection-based theorem proving in intuitionistic first-order logic (2005)
  16. Hodas, Joshua S.; Tamura, Naoyuki: lolliCoP -- a linear logic implementation of a lean connection-method theorem prover for first-order classical logic (2001)