A Non-clausal Connection Calculus

DOI10.1007/978-3-642-22119-4_18zbMath1333.03004MaRDI QIDQ3010371

Jens Otten

Publication date: 1 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22119-4_18

Mathematics Subject Classification ID

03B10: Classical first-order logic

03B35: Mechanization of proofs and logical operations

Related Items

From Schütte’s Formal Systems to Modern Automated Deduction, The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9, Incremental variable splitting, Machine learning guidance for connection tableaux, The possibilistic Horn non-clausal knowledge bases, The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics, nanoCoP: A Non-clausal Connection Prover

Uses Software

• leanCoP
• ileanCoP
• JProver

Cites Work

• Linearity and regularity with negation normal form
• Liberalized variable splitting
• A structure-preserving clause form translation
• IeanCOP: lean connection-based theorem proving
• Restricting backtracking in connection calculi
• Matings in matrices
• Theorem Proving via General Matings
• Automated Reasoning with Analytic Tableaux and Related Methods
• A Machine-Oriented Logic Based on the Resolution Principle
• Mechanical Theorem-Proving by Model Elimination
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item