A Non-clausal Connection Calculus

DOI10.1007/978-3-642-22119-4_18MaRDI QIDQ3010371zbMATH OpenOpenAlexFDO

Authors 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

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Recommendations

• Non-clausal connection calculi for non-classical logics
• Connections in nonclassical logics
• scientific article; zbMATH DE number 1950264
• scientific article; zbMATH DE number 1748570
• scientific article; zbMATH DE number 1341619
• Connection-based proof construction in non-commutative logic
• Nonstandard connectives of intuitionistic propositional logic
• Connection calculus theorem proving with multiple built-in theories
• scientific article; zbMATH DE number 5872259

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A structure-preserving clause form translation
• Automated Reasoning with Analytic Tableaux and Related Methods
• Connections in nonclassical logics
• scientific article; zbMATH DE number 1543301 (Why is no real title available?)
• scientific article; zbMATH DE number 1765687 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• IeanCOP: lean connection-based theorem proving
• Liberalized variable splitting
• Linearity and regularity with negation normal form
• Matings in matrices
• Mechanical Theorem-Proving by Model Elimination
• Model elimination and connection tableau procedures
• Restricting backtracking in connection calculi
• Tableaux and related methods
• Theorem Proving via General Matings

Cited in

(18)

• Non-clausal connection calculi for non-classical logics
• 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
• Certification of nonclausal connection tableaux proofs
• Connections in nonclassical logics
• nanoCoP: a non-clausal connection prover
• scientific article; zbMATH DE number 48763 (Why is no real title available?)
• scientific article; zbMATH DE number 1341619 (Why is no real title available?)
• Incremental variable splitting
• scientific article; zbMATH DE number 1950264 (Why is no real title available?)
• scientific article; zbMATH DE number 1552523 (Why is no real title available?)
• scientific article; zbMATH DE number 1748570 (Why is no real title available?)
• scientific article; zbMATH DE number 2169302 (Why is no real title available?)
• From Schütte’s Formal Systems to Modern Automated Deduction
• The 9th IJCAR automated theorem proving system competition -- CASC-J9
• Automated Reasoning with Analytic Tableaux and Related Methods
• Controlled use of clausal lemmas in connection tableau calculi

Describes a project that uses

Uses Software

• leanCoP
• ileanCoP
• JProver

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3010371)