Redundancy criteria for constrained completion

DOI10.1007/978-3-662-21551-7_2zbMath1503.68293OpenAlexW4299522952MaRDI QIDQ5055781

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/978-3-662-21551-7_2

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Using forcing to prove completeness of resolution and paramodulation
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Critical pair criteria for completion
• Equational problems and disunification
• Unnecessary inferences in associative-commutative completion procedures
• Rewrite-based Equational Theorem Proving with Selection and Simplification