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

DOI10.1145/138027.138032zbMath0779.68050DBLPjournals/jacm/GallierNPRS93OpenAlexW2056181378WikidataQ29029918 ScholiaQ29029918MaRDI QIDQ4033833

Jean H. Gallier, Stan Raatz, Wayne Snyder, Paliath Narendran, David Alan 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

zbMATH Keywords

completion procedureground equations

Mathematics Subject Classification ID

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

Related Items (16)

Effective codescent morphisms in the varieties determined by convergent term rewriting systems. ⋮ Congruence Closure of Compressed Terms in Polynomial Time ⋮ Fine-grained concurrent completion ⋮ Intersection of finitely generated congruences over term algebra ⋮ Term rewriting restricted to ground terms. ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Canonicity! ⋮ Engineering DPLL(T) + Saturation ⋮ Canonical Ground Horn Theories ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Completion of rewrite systems with membership constraints ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ Congruential complements of ground term rewrite systems ⋮ 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