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

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

1 2 next

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

1 2 next