An algorithm for finding canonical sets of ground rewrite rules in polynomial time
From MaRDI portal
Publication:4033833
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
