nanoCoP: A Non-clausal Connection Prover
From MaRDI portal
Publication:2817929
DOI10.1007/978-3-319-40229-1_21zbMath1475.68445MaRDI QIDQ2817929
Publication date: 5 September 2016
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-40229-1_21
03B35: Mechanization of proofs and logical operations
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Related Items
From Schütte’s Formal Systems to Modern Automated Deduction, The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9, nanoCoP, Machine learning guidance for connection tableaux, The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics, Eliminating models during model elimination
Uses Software
Cites Work
- Linearity and regularity with negation normal form
- Liberalized variable splitting
- A structure-preserving clause form translation
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- IeanCOP: lean connection-based theorem proving
- lean\(T^ AP\): Lean tableau-based deduction
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- A Non-clausal Connection Calculus
- MleanCoP: A Connection Prover for First-Order Modal Logic
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Restricting backtracking in connection calculi
- Matings in matrices
- Theorem Proving via General Matings
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
