Efficient ground completion

DOI10.1007/3-540-51081-8_123zbMath1503.68156OpenAlexW210557330MaRDI QIDQ5055736

Wayne Snyder

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/3-540-51081-8_123

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Unnamed Item ⋮ Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems ⋮ Any ground associative-commutative theory has a finite canonical system ⋮ A fast algorithm for constructing a tree automaton recognizing a congruential tree language ⋮ Decidability and complexity of simultaneous rigid E-unification with one variable and related results ⋮ Logic with equality: Partisan corroboration and shifted pairing ⋮ On the duality of abduction and model generation in a framework for model generation with equality

Cites Work

• Unnamed Item
• Unnamed Item
• Rigid E-unification: NP-completeness and applications to equational matings
• Termination of rewriting
• The Church-Rosser property for ground term-rewriting systems is decidable
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Solvable cases of the decision problem
• Fast Decision Procedures Based on Congruence Closure
• Theorem Proving via General Matings
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Variations on the Common Subexpression Problem
• An algorithm for reasoning about equality
• Theorem proving using equational matings and rigid E -unification
• Tree-Manipulating Systems and Church-Rosser Theorems

This page was built for publication: Efficient ground completion