Efficient ground completion

DOI10.1007/3-540-51081-8_123MaRDI QIDQ5055736zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• An algorithm for finding canonical sets of ground rewrite rules in polynomial time
• On the complexity of recursive path orderings
• scientific article; zbMATH DE number 3928345
• Algorithms and reductions for rewriting problems. II.
• A fast algorithm for generating reduced ground rewriting systems from a set of ground equations

Cites work

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

Cited in

(10)

• A fast algorithm for constructing a tree automaton recognizing a congruential tree language
• On the duality of abduction and model generation in a framework for model generation with equality
• Decidability and complexity of simultaneous rigid E-unification with one variable and related results
• Logic with equality: Partisan corroboration and shifted pairing
• An algorithm for finding canonical sets of ground rewrite rules in polynomial time
• Completeness of tree automata completion
• Any ground associative-commutative theory has a finite canonical system
• On the complexity of recursive path orderings
• A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
• Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems

This page was built for publication: Efficient ground completion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055736)