nanoCoP: a non-clausal connection prover. nanoCoP is a compact non-clausal automated theorem prover for classical first-order logic. It is based on the non-clausal connection calculus for classical logic. More details about the calculus can be found in the documentation. Features of nanoCoP: Theorem prover for classical first-order logic with equality. Based on the non-clausal connection calculus. Proof search on the original formula structure. Implemented in Prolog. Sound and complete. Decision procedure for propositional logic. Strong performance. Simple first-order form input format (leanCoP or TPTP). Output of compact non-clausal connection proof. Available under the GNU general public license.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
- Färber, Michael; Kaliszyk, Cezary: Certification of nonclausal connection tableaux proofs (2019)
- Rawson, Michael; Reger, Giles: A neurally-guided, parallel theorem prover (2019)
- Sutcliffe, Geoff: The 9th IJCAR automated theorem proving system competition -- CASC-J9 (2018)
- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
- Otten, Jens: Nanocop: a non-clausal connection prover (2016)