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