nanoCoP: A Non-clausal Connection Prover

DOI10.1007/978-3-319-40229-1_21zbMath1475.68445OpenAlexW2484885137MaRDI QIDQ2817929

Jens Otten

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Eliminating models during model elimination ⋮ The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ Machine learning guidance for connection tableaux ⋮ nanoCoP ⋮ From Schütte’s Formal Systems to Modern Automated Deduction

Uses Software

• TPTP
• Prover9
• leanCoP
• ileanCoP
• JProver
• leanTAP
• E Theorem Prover
• FEMaLeCoP
• MleanCoP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: nanoCoP: A Non-clausal Connection Prover