A semantic backward chaining proof system

DOI10.1016/0004-3702(92)90044-XMaRDI QIDQ1193483zbMATH OpenOpenAlexFDO

Authors Xumin Nie, David A. Plaisted

Publication date 27 September 1992

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0004-3702(92)90044-x

zbMATH Keywords

cachingbackward chainingsplitting rulegenuine supportsemantic deletionsequent style clause-based system

Mathematics Subject Classification ID

Recommendations

• A complete semantic back chaining proof system
• scientific article; zbMATH DE number 4164185
• A semantical view of proof systems
• Backchain iteration: Towards a practical inference method that is simple enough to be proved terminating, sound, and complete
• A formal framework for specifying sequent calculus proof systems
• A framework for proof systems
• Proving structural properties of sequent systems in rewriting logic
• A semantic basis for proof queries and transformations
• Forward and backward chaining in linear logic. (Extended abstract)

Cites work

• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (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?)
• 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
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• A sequent-style model elimination strategy and a positive refinement
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Hierarchical deduction
• Non-Horn clause logic programming without contrapositives
• Schubert's steamroller problem: Formulations and solutions
• Using sophisticated models in resolution theorem proving

Cited in

(6)

• A typed resolution principle for deduction with conditional typing theory
• Eliminating redundant search space on backtracking for forward chaining theorem proving
• A Logical Characterization of Forward and Backward Chaining in the Inverse Method
• Semantically guided first-order theorem proving using hyper-linking
• scientific article; zbMATH DE number 4164185 (Why is no real title available?)
• A complete semantic back chaining proof system

Describes a project that uses

Uses Software

• OTTER

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

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