A completion procedure for conditional equations
From MaRDI portal
Publication:758211
DOI10.1016/S0747-7171(08)80132-0zbMath0724.68053MaRDI QIDQ758211
Publication date: 1991
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Related Items
Proving semantical equivalence of data specifications, Order-sorted completion: The many-sorted way, Efficient deduction in equality Horn logic by Horn-completion, Deductive and inductive synthesis of equational programs, Linear and unit-resulting refutations for Horn theories, Specification and proof in membership equational logic
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Conditional rewrite rules
- Termination of rewriting
- Conditional rewrite rules: Confluence and termination
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Solvable cases of the decision problem
- Proving termination with multiset orderings
- Proof normalization for resolution and paramodulation
- Completion of first-order clauses with equality by strict superposition
- Clausal rewriting