Redundancy criteria for constrained completion
From MaRDI portal
Publication:673620
DOI10.1016/0304-3975(94)00274-6zbMath0873.68189MaRDI QIDQ673620
Publication date: 28 February 1997
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(94)00274-6
DB lookup for MSC labels failed
Related Items
Cites Work
- Unnamed Item
- Unnamed Item
- 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
- A proof theory for general unification
- Unnecessary inferences in associative-commutative completion procedures
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Consider only general superpositions in completion procedures
- SOLVING SYMBOLIC ORDERING CONSTRAINTS