Proof normalization for resolution and paramodulation

DOI10.1007/3-540-51081-8_97zbMath1503.03015OpenAlexW1516274846MaRDI QIDQ5055708

Leo Bachmair

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-51081-8_97

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42)

Related Items (5)

Reduction techniques for first-order reasoning ⋮ Conditional rewriting in focus ⋮ Goal directed strategies for paramodulation ⋮ Using forcing to prove completeness of resolution and paramodulation ⋮ A completion procedure for conditional equations

Cites Work

• Orderings for term-rewriting systems
• Termination of rewriting
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Proving termination with multiset orderings
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Proving Theorems with the Modification Method
• Resolution Strategies as Decision Procedures
• Proving refutational completeness of theorem-proving strategies
• A Machine-Oriented Logic Based on the Resolution Principle
• The Concept of Demodulation in Theorem Proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof normalization for resolution and paramodulation