A complete semantic back chaining proof system

DOI10.1007/3-540-52885-7_76zbMath1509.68315MaRDI QIDQ6488519

David Alan Plaisted, Xumin Nie

Publication date: 28 April 2023

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Hierarchical deduction
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Non-Horn clause logic programming without contrapositives
• Using sophisticated models in resolution theorem proving
• A Semantically Guided Deductive System for Automatic Theorem Proving
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• A Simplified Format for the Model Elimination Theorem-Proving Procedure

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