An algorithm for finding canonical sets of ground rewrite rules in polynomial time

DOI10.1145/138027.138032zbMATH Open0779.68050DBLPjournals/jacm/GallierNPRS93OpenAlexW2056181378WikidataQ29029918 ScholiaQ29029918MaRDI QIDQ4033833FDOQ4033833

Authors: Jean Gallier, Paliath Narendran, Stan Raatz, Wayne Snyder, David A. Plaisted 

Publication date: 16 May 1993

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/138027.138032

Recommendations

• Efficient ground completion
• scientific article; zbMATH DE number 4080962
• On the complexity of recursive path orderings
• scientific article; zbMATH DE number 44069
• scientific article; zbMATH DE number 3928345

zbMATH Keywords

completion procedureground equations

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42)

Cited In (26)

• Completion of rewrite systems with membership constraints
• On the complexity of recursive path orderings
• SCL(EQ): SCL for first-order logic with equality
• Intersection of finitely generated congruences over term algebra
• Canonical ground Horn theories
• Effective codescent morphisms in the varieties determined by convergent term rewriting systems.
• Congruential complements of ground term rewrite systems
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• Title not available (Why is that?)
• On deciding satisfiability by theorem proving with speculative inferences
• A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
• Fine-grained concurrent completion
• Title not available (Why is that?)
• Title not available (Why is that?)
• Canonicity!
• Order-Sorted Rewriting and Congruence Closure
• Applying term rewriting methods to finite groups
• Efficient ground completion
• Linear completion
• Title not available (Why is that?)
• Title not available (Why is that?)
• Term rewriting restricted to ground terms.
• Congruence closure of compressed terms in polynomial time
• Engineering DPLL(T) + Saturation
• Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
• Deciding the word problem for ground identities with commutative and extensional symbols

This page was built for publication: An algorithm for finding canonical sets of ground rewrite rules in polynomial time

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