Goal directed strategies for paramodulation

DOI10.1007/3-540-53904-2_93MaRDI QIDQ5055756zbMATH OpenOpenAlexFDO

Authors

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)

Recommendations

• Basic paramodulation
• scientific article; zbMATH DE number 1348470
• Simultaneous paramodulation
• scientific article; zbMATH DE number 3837990
• On paramodulation in linear strategies of the resolution method

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• An Efficient Unification Algorithm
• An improved general E-unification method
• An inference system for horn clause logic with equality
• Complete sets of transformations for general E-unification
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Higher order E-unification
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 4045129 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 3330761 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• On restrictions of ordered paramodulation with simplification
• Proof normalization for resolution and paramodulation
• Proving refutational completeness of theorem-proving strategies
• Proving Theorems with the Modification Method

Cited in

(10)

• Basic paramodulation
• Paramodulation-based theorem proving
• scientific article; zbMATH DE number 3837990 (Why is no real title available?)
• On paramodulation in linear strategies of the resolution method
• scientific article; zbMATH DE number 1754647 (Why is no real title available?)
• Superposition for lambda-free higher-order logic
• Set-of-support strategy for higher-order logic
• Simultaneous paramodulation
• Superposition with Delayed Unification
• SAD as a mathematical assistant -- how should we go from here to there?

This page was built for publication: Goal directed strategies for paramodulation

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