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 24 articles , 1 standard article )

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

1 2 next

  1. Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
  2. Ebner, Gabriel: Herbrand constructivization for automated intuitionistic theorem proving (2019)
  3. Färber, Michael; Kaliszyk, Cezary: Certification of nonclausal connection tableaux proofs (2019)
  4. Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef: ProofWatch: watchlist guidance for large theories in E (2018)
  5. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
  6. Gilbert, Frédéric: Automated constructivization of proofs (2017)
  7. Sutcliffe, Geoff: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (2017)
  8. Färber, Michael; Brown, Chad: Internal guidance for Satallax (2016)
  9. Freitas, Fred; Otten, Jens: A connection calculus for the description logic ( \mathcalALC) (2016)
  10. Otten, Jens: Nanocop: a non-clausal connection prover (2016)
  11. Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
  12. Kaliszyk, Cezary; Urban, Josef: FEMaLeCoP: fairly efficient machine learning connection prover (2015)
  13. Schulz, Stephan; Sutcliffe, Geoff: Proof generation for saturating first-order theorem provers (2015)
  14. Otten, Jens: MleanCoP: a connection prover for first-order modal logic (2014)
  15. Alonderis, R.: A proof-search procedure for intuitionistic propositional logic (2013)
  16. Benzmüller, Christoph; Raths, Thomas: HOL based first-order modal logic provers (2013)
  17. Benzmüller, Christoph; Otten, Jens; Raths, Thomas: Implementing and evaluating provers for first-order modal logics (2012)
  18. Otten, Jens: A non-clausal connection calculus (2011)
  19. Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr: MaLeCoP. Machine learning connection prover (2011)
  20. Brandt, Christoph; Otten, Jens; Kreitz, Christoph; Bibel, Wolfgang: Specifying and verifying organizational security properties in first-order logic (2010)

1 2 next