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 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
- Alonderis, R.: A proof-search procedure for intuitionistic propositional logic (2013)
- Brandt, Christoph; Otten, Jens; Kreitz, Christoph; Bibel, Wolfgang: Specifying and verifying organizational security properties in first-order logic (2010)
- Otten, Jens: Restricting backtracking in connection calculi (2010)
- Otten, Jens: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic. (System descriptions) (2008)
- Otten, Jens: Clausal connection-based theorem proving in intuitionistic first-order logic (2005)
- Hodas, Joshua S.; Tamura, Naoyuki: lolliCoP -- a linear logic implementation of a lean connection-method theorem prover for first-order classical logic (2001)