Goal directed strategies for paramodulation

DOI10.1007/3-540-53904-2_93zbMath1503.68295OpenAlexW1585276220MaRDI QIDQ5055756

No author found.

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-53904-2_93

Mathematics Subject Classification ID

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

Related Items

SAD as a mathematical assistant -- how should we go from here to there? ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Complete sets of transformations for general E-unification
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• An Efficient Unification Algorithm
• Proving Theorems with the Modification Method
• Proving refutational completeness of theorem-proving strategies
• Proof normalization for resolution and paramodulation
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• A Machine-Oriented Logic Based on the Resolution Principle
• An inference system for horn clause logic with equality