A complete semantic back chaining proof system

DOI10.1007/3-540-52885-7_76MaRDI QIDQ6488519zbMATH OpenFDO

Authors Xumin Nie, David A. Plaisted

Publication date 28 April 2023

Full work available at URL https://doi.org/10.1007/3-540-52885-7_76

Mathematics Subject Classification ID

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

Recommendations

• A semantic backward chaining proof system
• scientific article; zbMATH DE number 4164185
• scientific article; zbMATH DE number 3935002
• A sequent-style model elimination strategy and a positive refinement
• The search efficiency of theorem proving strategies

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• A Semantically Guided Deductive System for Automatic Theorem Proving
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Hierarchical deduction
• scientific article; zbMATH DE number 3774914 (Why is no real title available?)
• scientific article; zbMATH DE number 3343519 (Why is no real title available?)
• scientific article; zbMATH DE number 3185223 (Why is no real title available?)
• Non-Horn clause logic programming without contrapositives
• Using sophisticated models in resolution theorem proving

Cited in

(3)

• A semantic backward chaining proof system
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• scientific article; zbMATH DE number 4164185 (Why is no real title available?)

This page was built for publication: A complete semantic back chaining proof system

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