A fast algorithm for generating reduced ground rewriting systems from a set of ground equations

DOI10.1006/jsco.1993.1029zbMath0804.68072OpenAlexW2037163667MaRDI QIDQ689111

Wayne Snyder

Publication date: 6 December 1993

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jsco.1993.1029

zbMATH Keywords

simplificationterm rewriting systemcongruence closureground equations

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (16)

Deciding confluence of certain term rewriting systems in polynomial time ⋮ Congruence Closure of Compressed Terms in Polynomial Time ⋮ Fine-grained concurrent completion ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Intersection of finitely generated congruences over term algebra ⋮ Term rewriting restricted to ground terms. ⋮ On ground tree transformations and congruences induced by tree automata. ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Symbol different term rewrite systems ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Deterministic bottom-up tree transducers and ground term rewrite systems ⋮ CHAP and rewrite components ⋮ Congruential complements of ground term rewrite systems ⋮ Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols ⋮ Restricted ground tree transducers ⋮ Deciding the word problem for ground identities with commutative and extensional symbols

This page was built for publication: A fast algorithm for generating reduced ground rewriting systems from a set of ground equations