Proof normalization for resolution and paramodulation

DOI10.1007/3-540-51081-8_97MaRDI QIDQ5055708zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 1082077
• On proof normalization in linear logic
• scientific article; zbMATH DE number 3986670
• Proof normalization with nonstandard objects
• Some general results about proof normalization
• scientific article; zbMATH DE number 874672
• Paramodulation-based theorem proving
• scientific article; zbMATH DE number 1405619
• scientific article; zbMATH DE number 3950526
• scientific article; zbMATH DE number 4091495

Cites work

• scientific article; zbMATH DE number 4049135 (Why is no real title available?)
• scientific article; zbMATH DE number 4053061 (Why is no real title available?)
• scientific article; zbMATH DE number 4090851 (Why is no real title available?)
• scientific article; zbMATH DE number 3444822 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (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?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Orderings for term-rewriting systems
• Proving Theorems with the Modification Method
• Proving refutational completeness of theorem-proving strategies
• Proving termination with multiset orderings
• Resolution Strategies as Decision Procedures
• Termination of rewriting
• The Concept of Demodulation in Theorem Proving

Cited in

(9)

• A completion procedure for conditional equations
• Using forcing to prove completeness of resolution and paramodulation
• Rewrite method for theorem proving in first order theory with equality
• scientific article; zbMATH DE number 1538009 (Why is no real title available?)
• Goal directed strategies for paramodulation
• Normalization Proof for Derivations in PA after P. Cohen
• Reduction techniques for first-order reasoning
• scientific article; zbMATH DE number 3837990 (Why is no real title available?)
• Conditional rewriting in focus

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

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