Tiwari, A. (2009). Combining Equational Reasoning. In: Ghilardi, S., Sebastiani, R. (eds) Frontiers of Combining Systems. FroCoS 2009. Lecture Notes in Computer Science(), vol 5749. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04222-5_4
Abstract
Given a theory 𝕋T, a set of equations E, and a single equation e, the uniform word problem (UWP) is to determine if 𝐸⇒𝑒E⇒e in the theory 𝕋T. We recall the classic Nelson-Oppen combination result for solving the UWP over combinations of theories and then present a constructive version of this result for equational theories. We present three applications of this constructive variant. First, we use it on the pure theory of equality (𝕋𝐸𝑄TEQ) and arrive at an algorithm for computing congruence closure of a set of ground term equations. Second, we use it on the theory of associativity and commutativity (𝕋𝐴𝐶TAC) and obtain a procedure for computing congruence closure modulo AC. Finally, we use it on the combination theory 𝕋𝐸𝑄∪𝕋𝐴𝐶∪𝕋𝑃𝑅TEQ∪TAC∪TPR, where 𝕋𝑃𝑅TPR is the theory of polynomial rings, to present a decision procedure for solving the UWP for this combination.
Keywords: Inference Rule, Decision Procedure, Polynomial Ring, Function Symbol, Equational Theory