Decision procedures in automated deduction
Leo Bachmair, Ashish Tiwari · 2000
We present a practical variant of the Nelson-Oppen abstract combination result which can be used for combining decision procedures based on completion. We suitably instantiate this general theorem to obtain combinations of a class of congruence closure algorithms, procedures for deciding the word problem in ground AC-theories (generalization of the word problem for commutative semigroups), and algorithms for polynomial ideals over general rings. The combination result can also be used to integrate several other theories. Our description of abstract congruence closure suitably captures the logical essence of most of the conventional algorithms for congruence closure. Additionally, it can be used to obtain new efficient implementations. Experimental results are presented to illustrate the relative efficiency and explain differences in performance of these various algorithms. The transition rules for computation of abstract congruence closure are obtained from rules for standard completion enhanced with an extension rule that enlarges a given signature by new constants. We use our general combination result to define the notion of an associative-commutative congruence closure and give a complete set of transition rules for construction of such closures. This solves the word problem for ground AC-theories without the need for AC-simplification orderings total on ground terms. Associative-commutative congruence closure provides a novel way to construct a convergent rewrite system for a ground AC-theory. The concept of an abstract congruence closure also helps to clarify and generalize procedures that are based on congruence closure, for example construction of convergent rewrite systems, non-oblivious normalization, and the problem of rigid E-unification. Finally, we describe the Grobner bases based decision procedure for polynomial ideals using completion-like transition rules, which is a generalization of the theory of Grobner bases for polynomial ideals over fields to polynomials over commutative Noetherian rings. In the same spirit as what Grobner bases do for polynomials over fields, we can use the new generalization to solve several problems in the theory of multivariate polynomials over rings.