Redundancy criteria for constrained completion
From MaRDI portal
Publication:673620
DOI10.1016/0304-3975(94)00274-6zbMath0873.68189OpenAlexW2091691231MaRDI 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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Rewrite semantics for production rule systems: Theory and applications ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs ⋮ Local simplification ⋮ Local simplification
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Redundancy criteria for constrained completion
