Redundancy criteria for constrained completion
From MaRDI portal
Publication:5055781
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
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