A semantic backward chaining proof system
From MaRDI portal
Publication:1193483
DOI10.1016/0004-3702(92)90044-XzbMath0762.68056OpenAlexW2079135579MaRDI QIDQ1193483
Xumin Nie, David Alan 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
cachingbackward chainingsplitting rulegenuine supportsemantic deletionsequent style clause-based system
Related Items
Semantically guided first-order theorem proving using hyper-linking, A typed resolution principle for deduction with conditional typing theory
Uses Software
Cites Work
- A mechanical solution of Schubert's steamroller by many-sorted resolution
- Hierarchical deduction
- Schubert's steamroller problem: Formulations and solutions
- 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 sequent-style model elimination strategy and a positive refinement
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
