Proof normalization for resolution and paramodulation
From MaRDI portal
Publication:5055708
DOI10.1007/3-540-51081-8_97zbMath1503.03015OpenAlexW1516274846MaRDI QIDQ5055708
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
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