Patent Publication Number: US-2004049474-A1

Title: Method for combining decision procedures

Description:
RELATED APPLICATIONS  
     [0001] This application claims priority from co-pending U.S. Provisional Application Serial No. 60/397,201 filed Jul. 19, 2002. 
    
    
     REFERENCE TO GOVERNMENT FUNDING  
     [0002] This invention was made with Government support under Contract Number CA86370-02 awarded by the National Science Foundation. The Government has certain rights in this invention. 
    
    
     
       FIELD OF INVENTION  
       [0003] This invention teaches a decision procedure for combination of theories useful in automated deduction.  
       BACKGROUND OF THE INVENTION  
       [0004] The following papers provide useful background information, for which they are incorporated herein by reference in their entirety, and are selectively referred to in the remainder of this disclosure by their accompanying reference identifiers in square brackets (i.e., [BDS02] for the second listed paper, by Barrett et al).  
       [0005] [BDL96] Clark Barrett, David Dill, and Jeremy Levitt. Validity checking for combinations of theories with equality. In Mandayam Srivas and Albert Camilleri, editors,  Formal Methods in Computer - Aided Design  ( FMCAD  &#39;96), volume 1166 of  Lecture Notes in Computer Science,  pages 187-201, Palo Alto, Calif., November 1996. Springer-Verlag.  
       [0006] [BDS02] Clark W. Barrett. David L. Dill, and Aaron Stump. A generalization of Shostak&#39;s method for combining decision procedures. In A. Armando, editor,  Frontiers of Combining Systems,  4 th International Workshop, ProCos  2002, number 2309 in Lecture Notes in Artificial Intelligence, pages 132-146, Berlin, Germany, April 2002. Springer-Verlag.  
       [0007] [Bjø99] Nikolaj Bjøner.  Integrating Decision Procedures for Temporal Verification . PhD thesis, Stanford University, 1999.  
       [0008] [BS96] F. Baader and K. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures.  J. Symbolic Computation,  21: 211-243, 1996.  
       [0009] [BTV02] Leo Bachmair, Ashish Tiwari, and Laurent Vigneron. Abstract congruence closure.  Journal of Automated Reasoning,  2002. To appear.  
       [0010] [CLS96] David Cyrluk, Patrick Lincoln, and N. Shankar. On Shostak&#39;s decision procedure for combinations of theories. In M. A. McRobbie and J. K. Slaney, editors.  Automated Deduction—CADE -13, volume 1104 of  Lecture Notes in Artificial Intelligence,  pages 463-477, New Brunswick, N.J., July/August 1996. Springer-Verlag.  
       [0011] [DST80] P. J. Downey, R. Sethi, and R. E. Tarjan. Variations on the common subexpressions problem.  Journal of the ACM,  27(4):758-771, 1980.  
       [0012] [FORS01] J. C. Fillie,ãtre, S. Owre, H. Rueβ, and N. Shankar. ICS: Integrated Canonization and Solving. In G. Berry, H. Comon, and A. Finkel, editors,  Computer - Aided Verification, CAV &#39; 2001, volume 2102 of  Lecture Notes in Computer Science,  pages 246-249, Paris, France, July 2001. Springer-Verlag.  
       [0013] [FS02] Jonathan Ford and Natarajan Shankar. Formal verification of a combination decision procedure. In A. Voronkov, editor,  Proceedings of CADE -19, Berlin, Germany, 2002. Springer-Verlag.  
       [0014] [Gan02] Harald Ganzinger. Shostak light. In A. Voronkov, editor,  Proceedings of CADE -19, Berlin, Germany, 2002. Springer-Verlag.  
       [0015] [Kap97] Deepak Kapur. Shostak&#39;s congruence closure as completion. In H. Comon, editor,  International Conference on Rewriting Techniques and Applications, RTA  &#39;97, number 1232 in Lecture Notes in Computer Science, pages 23-37, Berlin, 1997. Springer-Verlag.  
       [0016] [Kos77] Dexter Kozen. Complexity of finitely presented algebras. In  Conference Record of the Ninth Annual A CM Symposium on Theory of Computing,  pages 164-177, Boulder, Colo., May 2-4, 1977.  
       [0017] [Lev99] Jeremy R. Levitt.  Formal Verification Techniques for Digital Systems.  PhD thesis, Stanford University, 1999.  
       [0018] [N079] G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures.  ACM Transactions on Programming Languages and Systems,  1(2):245-257, 1979.  
       [0019] [N080] G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. Journal  of the ACM,  27(2):356-364, 1980.  
       [0020] [RS01] Harald Rueβ and Natarajan Shankar. Deconstructing Shostak. In 16 th Annual IEEE Symposium on Logic in Computer Science,  pages 19-28, Boston, Mass., July 2001. IEEE Computer Society.  
       [0021] [Sha01] Natarajan Shankar. Using decision procedures with a higher-order logic. In Theorem  Proving in Higher Order Logics:  14 th International Conference, TPHOLs  2001,  volume  2152 of  Lecture Notes in Computer Science,  pages 5-26, Edinburgh, Scotland, September 2001. Springer-Verlag.  
       [0022] [Sho78] R. Shostak. An algorithm for reasoning about equality.  Comm. ACM,  21:583-585, July 1978.  
       [0023] [Sho84] Robert E. Shostak. Deciding combinations of theories.  Journal of the ACM,  31(1):1-12, January 1984.  
       [0024] [Tiw00] Ashish Tiwari.  Decision Procedures in Automated Deduction.  PhD thesis, State University of New York at Stony Brook, 2000.  
       [0025] A decision procedure determines if a given logical formula is valid. Such formulas can be built from  
       [0026] 1. Variables: x, y, z, etc.  
       [0027] 2. Function symbols like addition (+) and multiplication (*)  
       [0028] 3. Predicate symbols like those for equality (=) and inequality (&lt;, &gt;, ≦, ≧)  
       [0029] 4. Propositional connectives for negation ( ), conjunction ( ), disjunction ( ), and implication ( ), and  
       [0030] 5. Universal and existential quantifiers (∀, ∃).  
       [0031] A ground decision procedure deals solely with quantifier-free formulas where all the variables in the formula are implicitly universally quantified at the outermost level. Since a quantifier-free formula can be placed into conjunctive normal form as a conjunction of disjunctions (clauses) consisting of atomic formulas (equalities, inequalities, etc.) and their negations, it is sufficient to separately determine the validity of each such clause. The validity of a clause l 1     . . .   l n , where each l i  is either an atomic formula or its negation, can be decided by determining the satisfiability of  l 1     . . .    l n . The latter conjunction is unsatisfiable if and only if the former disjunction is valid.  
       [0032] The function and predicate symbols in a formula may be uninterpreted, such that the formula can be satisfied by assigning any interpretation (i.e., meaning of the symbol within the rules of a given theory) to these symbols. Some of the function and predicate symbols can also be interpreted with respect to a theory that assigns the symbol a specific interpretation. For example, one usual interpretation of the function symbol “+” corresponds to the arithmetic meaning (addition) of the symbol and if assigned this interpretation it cannot be assigned the same interpretation as other operations, like those of taking maximum or minimum of two numbers. Formulas can contain a mixture of symbols that are uninterpreted or from one of several theories such as those for arithmetic, lists, arrays, and bit-vectors. Many proof obligations arising from applications such as automated verification, program optimization, and test-case generation, involve constraints from a combination of theories. A combination decision procedure is one that can decide formulas in a combination of theories, and a combination method is one that can be used to assemble a combination decision procedure from individual decision procedures. In the inventive method, the individual theories must be disjoint, so that no function symbol is interpreted in more than one theory. However this is not a problem in practice, as a preprocessing step can be used to disambiguate symbols through, for example, typechecking to differentiate a use of “+” as arithmetic addition and list concatentation.  
       [0033] Ground decision procedures for combination of theories are used in many systems for automated deduction. Two basic paradigms exist for combining decision procedures: Nelson Oppen and Shostak. The Nelson Oppen method combines decision procedures for disjoint theories by exchanging the equality information on the shared variables. In Shostak&#39;s method, the combination of the theory of pure equality with canonizable and solvable theories is decided through an extension of congruence closure, that yields a canonizer for the combined theory. However, Shostak&#39;s method and all subsequent implementations and use of the method are seriously flawed. What is needed is a correct method to combine multiple disjoint canonizable solvable theories within a Shostak-like framework.  
       SUMMARY OF THE INVENTION  
       [0034] The invention addresses the satisfiability of conjunctions of equalities and disequalities. It is based on the Shostak approach of using canonizers and solvers, and handles the general combination of several theories and uninterpreted symbols. It is sound, in the sense that when it asserts that a formula is unsatisfiable, the formula is indeed unsatisfiable. It is also complete and terminating. The decision procedure is an online method, in that it processes each equality or disequality as it given and either signals a contradiction indicating unsatisfiability, or constructs a state capturing the information contained in the given formulas. The state S consists of a solution set S i  for each theory θ i  and a solution set S V  for equalities between variables. The state thus constructed is used to construct a canonizer S[[a]], an operation that simplifies a given expression a to a canonical form a′ so that two expressions that are equal under the given information possess the same canonical form. The critical challenge in the construction of such a canonizer is that of computing a canonical form for a variable x given that such a variable might have a solution in more than one component solution set. The solution returned by the canonizer is context-sensitive so that if x occurs as ƒ(x) for a symbol ƒ from theory θ i , then the solution for x from S i  is used.  
       [0035] Each input formula is either an equality a=b or a disequality a≠b. Each input equality is processed with respect to the current state to yield a new state. A disequality a≠b is checked with respect to the new state s by computing the canonical forms s[[a]] and s[[b]] and checking if they are identical. An input equality a=b is processed by first computing the canonical forms a′=b′, where a′ is s[[a]] and b′ is s[[b]]. The canonized equality a′=b′ is then variable abstracted. Variable abstraction is applied to a′=b′ by successively replacing each maximally pure subterm c by a new variable x and adding x=c to the theory θ corresponding to c. A maximally pure subterm of the equality is one whose function symbols are all from a single theory θ and that is not a subterm of some other pure term. Variable abstraction eventually turns the equality a′=b′ into an equality between variables x=y. This equality can be added to S V  to merge the partitions corresponding to variables x and y. This merger can lead to further equalities since the solutions a x  and a y  for x and y, respectively, in some solution set S i  might be distinct. A closure operation is used to propagate the equality of x and y to S i  by solving the equality a x =a y  using solve i  and composing the solution into S i . The use of the solver might yield a contradiction, as in an attempt to solve z=z+1. The closure operation can also yield new equalities between variables that are propagated back to S V . The closure operation is applied repeatedly until no further equalities are left to be propagated. The resulting closed state S either contains an explicit contradiction or is in a form that is suitable for use in the canonizer.  
       [0036] The method provides a sound and complete online decision method for the combination of canonizable and solvable theories together with uninterpreted function and predicate symbols. It also provides the representation of a solution state in terms of theory-wise solution sets that are used to capture the equality information extracted from the processed equalities. The method includes a context-sensitive canonizer that uses theory-specific canonizers and the solution state to obtain the canonical form of an expression with respect to the given equality information. Moreover, included is the variable abstraction operation for reducing and equality between term to an equality between variables and an enhanced solution state. The closure operation for propagating equality information between solution sets for individual theories uses the theory-specific solvers. The invention teaches a modular method for combining solvers and canonizers into a combination decision procedure. Furthermore, the modular method is useful for integrating Shostak-style decision procedures within a Nelson-Oppen combination so that equality information can be exchanged between theories that are canonizable and solvable, and those that are not.  
       [0037] The invention provides a method for deciding a formula with respect to a state comprising: canonizing the formula to create a canonical formula; abstracting the variables in the canonical formula and the state to create an abstracted formula and an abstracted state; asserting the abstracted formula into the abstracted state to create an asserted state; and closing the asserted state. In one aspect, the invention further provides a further step of signaling a contradiction between the formula and the state, indicating unsatisfiability of the formula. In another aspect, the method of the invention may be used as a decision procedure within a Nelson-Oppen framework. Preferred embodiments of the invention perform abstraction by reducing an equality between terms to an equality between variables and an enhanced solution state. Further preferred embodiments of the invention are operable in a modular manner so as to combine solvers and canonizers into a combination decision procedure. In another aspect, the formula to be decided contains uninterpreted function and predicate symbols; and in another aspect the formula contains symbols from more than one interpreted theory. In preferred embodiments of the invention the interpreted theory is selected from the group consisting of arithmetic, lists, arrays and bitvectors. Preferred embodiments of the invention are operable in an online manner so as to process each formula as it is given. In another aspect, the formula to be decided is a proof obligation resulting from an application selected from the group consisting of automated verification, program optimization and test case generation.  
       [0038] Further provided is a method for closing a set of sets of formulas, such set of sets containing a variable equality state set, an uninterpreted theory state set and one or more theory state sets comprising: merging any equalities present in the one or more theory state sets that are not present in the variable equality state set into the variable equality state set and into the uninterpreted theory state set; merging any equalities present in the variable equality state set that are not present in the one or more theory state sets into said one or more theory state sets; and normalizing the one or more theory state sets. In another aspect, the step of merging any equalities present in the variable equality state set that are not present in the one or more theory state sets merges the equality after the application of a theory-specific solver.  
       [0039] The invention also provides a method for canonizing a term with respect to a theory state comprising: canonizing all subterms of the term to create canonical subterms; interpreting said canonical subterms to create interpreted canonical subterms; creating a second term from the application of the operator of the first term to the interpreted canonical subterms; applying a theory specific canonizer to the second term to create a theory specific canonized term; determining if the theory specific canonized term is the right hand side of an equality in said theory state and if so returning the left hand side of the equality, otherwise returning the theory specific canonized term. 
     
    
    
     BRIEF DESCRIPTION OF THE DRAWINGS  
     [0040]FIG. 1 is a flow chart illustrative of the inventive method.  
     [0041]FIG. 2 is a flow chart that schematically illustrates the inventive method.  
     [0042]FIG. 3 is a flow chart that further illustrates the inventive method of FIGS. 1 and 2.  
    
    
     DETAILED DESCRIPTION OF THE INVENTION  
     [0043]FIG. 1 is a flow chart that schematically illustrates a method for deciding a formula  20  with respect to a state  22  comprising: at step  24 , canonizing the formula to create a canonical formula  26 ; at step  30 , abstracting the variables in the canonical formula  26  and the state  28  to create an abstracted formula  32  and an abstracted state  34 ; at step  36 , asserting the abstracted formula  32  into said abstracted state  34  to create an asserted state  38 ; and at step  40  closing the asserted state  38 , where closing means repeating the close step  40  until there is no further change in state.  
     [0044]FIG. 2 schematically illustrates a method for closing a set of sets of formulas, such set of sets containing a variable equality state set, an uninterpreted theory state set and one or more theory state sets comprising: at step  50 , merging any equalities present in the one or more theory state sets that are not present in the variable equality state set into the variable equality state set and into the uninterpreted theory state set; at step  52 , merging any equalities present in the variable equality state set that are not present in the one or more theory state sets into one or more theory state sets; and at step  54 , normalizing the one or more theory state sets.  
     [0045]FIG. 3 schematically illustrates a method for canonizing a term provided at step  60  with respect to a theory state comprising: at step  62  canonizing all subterms of the term to create canonical subterms; at step  64 , interpreting said canonical subterms to create interpreted canonical subterms and creating a second term from the application of the operator of the first term to the interpreted canonical subterms; at step  66 , applying a theory specific canonizer to the second term to create a theory specific canonized term; at step  68 , determining if the theory specific canonized term is ( 70 ) or is not ( 72 ) the right hand side of an equality in the theory state and if so returning the left hand side of the equality at step  74 , otherwise returning the theory specific canonized term at step  76 .  
     [0046] Consider the sequent 
     2* car ( x )−3* cdr ( x )=ƒ( cdr ( x )) 
     ƒ( cons (4* car ( x )−2*ƒ( cdr ( x )), y ))=ƒ( cons (6* cdr ( x ), y )). 
     [0047] It involves symbols from three different theories. The symbol ƒ is uninterpreted, the operations * and − are from the theory of linear arithmetic, and the pairing and projection operations cons, car, and cdr, are from the theory of lists (using the traditional names from the Lisp programming language). There are two basic methods for building combined decision procedures for disjoint theories, i.e., theories that share no function symbols. Nelson and Oppen [NO79] gave a method for combining decision procedures through the use of variable abstraction for replacing subterms with variables, and the exchange of equality information on the shared variables. Thus, with respect to the example above, decision procedures for pure equality, linear arithmetic, and the theory of lists can be composed into a decision procedure for the combined theory. The other combination method, due to Shostak, yields a decision procedure for the combination of canonizable and solvable theories, based on the congruence closure procedure. Shostak&#39;s original algorithm and proof were seriously flawed. His algorithm is neither terminating nor complete (even when terminating). These flaws went unnoticed for a long time even though the method was widely used, implemented, and studied [CLS96, BDL96, Bjø99]. In earlier work [RSO1], a correct algorithm was described for the basic combination of a single canonizable, solvable theory with the theory of equality over uninterpreted terms. That correctness proof has been mechanically verified using PVS [FS02]. The generality of the basic combination (i.e., its applicability to multiple theories) rests on Shostak&#39;s claim that it is possible to combine solvers and canonizers from disjoint theories into a single canonizer and solver. This claim is easily verifiable for canonizers, but is false for the case of solvers. Using the inventive method, earlier decision procedures may be extended to the combination of uninterpreted equality with multiple canonizable, solvable theories. The decision procedure does not require the combination of solvers. Proofs for the termination, soundness, and completeness of the procedure are included.  
     [0048] 2 Preliminaries  
     [0049] Some basic terminology is needed to understand Shostak style decision procedures. Fixing a countable set of variables X and a set of function symbols F, a term is either a variable x from X or a n-ary function symbol ƒ from F applied to n terms as in ƒ(a 1 , . . . a n ). Equations between terms are represented as a=b. Let vars(a), vars(a=b), and vars(T) represent the sets of variables in a, a=b, and the set of equalities T, respectively. Of interest is deciding the validity of sequents of the form T|−c=d where c and d are terms, and T is a set of equalities such that vars(c=d) ⊂ vars(T). The condition vars(c=d) ⊂ vars(T) is there for technical reasons. It can always be satisfied by padding T with reflexivity assertions x=x for any variables x in vars(c=d)−vars(T). One writes ┌a┐ for the set of subterms of a, which includes a.  
     [0050] The semantics for a term a, written as M[a]ρ, is given relative to an interpretation M over a domain D and an assignment ρ. For an n-ary function ƒ, the interpretation M(ƒ) of ƒ in M is a map from D n  to D. For an uninterpreted n-ary function symbol ƒ, the interpretation M(ƒ) may be any map from D n  to D, whereas only restricted interpretations might be suitable for an interpreted function symbol like the arithmetic+operation. An assignment ρ is a map from variables in X to values in D. M[a]ρ is defined to return a value in D by means of the following equations. 
       M[x]ρ=ρ ( x ) 
       M[ƒ ( a   1   , . . . , a   n )]ρ= M (ƒ)( M[a   1   ]ρ, . . . , M[a   n ]ρ) 
     [0051] It is said that M,ρ a=b iƒƒM[a]ρ=M[b]ρ, and M a=b iƒƒM, ρ a=b for all assignments ρ. It is written M,ρ S when ∀a,b: a=b∈S M, ρ a=b, and M,ρ (T a=b) when (M,ρ T) (M,ρ a=b). A sequent T c=d is valid, written as  (T c=d), when M,ρ T c=d), for all M and ρ.  
     [0052] There is a simple pattern underlying the class of decision procedures studied here. Let ψ be the state of the decision procedure as given by a set of formulas. 1  Let τ be a family of state transformations so that ψ ψ′ if ψ′ is the result of applying a transformation in τ to ψ, where vars(ψ) ⊂ vars(ψ′) (variable preservation). An assignment ρ′ is said to extend ρ over vars(ψ′)−vars(ψ) when it agrees with ρ on all variables except those in vars(ψ′)−vars(ψ) for vars(ψ) ⊂ vars(ψ′). ψ′ preserves ψ if vars(ψ) ⊂ vars(ψ′) and for all interpretations M and assignments ρ, M, ρ′ ψ holds iff there exists an assignment ρ′ extending ρ such that M,ρ′ ψ′. 2  When preservation is restricted to a limited class of interpretations ι, it is said that ψ′ ι-preserves ψ. Note that the preserves relation is transitive. When the operation τ is deterministic, τ(ψ) represents the result of the transformation, and τ is a conservative operation to indicate that τ(ψ) preserves ψ for all ψ. Correspondingly, τ is said to be ι-conservative when τ(ψ) ι-preserves ψ. Let τ n  represent the n-fold iteration of τ, then τ n  is a conservative operation. The composition, of τ 2 ∘τ 1  conservative operations τ 1  and τ 2 , is also a conservative operation. The operation τ*(ψ) is defined as τ i (ψ) for the least i such that τ i+1 (ψ)=τ i (ψ). The existence of such a bound i must be demonstrated for the termination of τ*. If τ is conservative, so is τ*.  
     [0053] If τ is a conservative operation, it is sound and complete in the sense that for a formula φ with vars(φ) ⊂ vars(ψ),  (ψ├φ) iff  (τ(ψ)├φ. This is clear since τ is a conservative operation and vars(φ) ⊂ vars(ψ).  
     [0054] If τ*(ψ) returns a state ψ′ such that  (ψ′├⊥). where ⊥ is an unsatisfiable formula, then ψ′ and ψ are both clearly unsatisfiable. Otherwise, if ψ′ is canonical, as explained below,  (ψ├φ) can be decided by computing a canonical form ψ′[φ] for φ with respect to ψ.  
     [0055] 3 Congruence Closure  
     [0056] In this section, an exercise is presented for deciding equality over terms where all function symbols are uninterpreted, i.e., the interpretation of these operations is unconstrained. This means that a sequent T├c=d is valid, i.e.,  (T├c=d) iff for all interpretations M and assignments ρ, the satisfaction relation M,ρ  (T├c=d) holds. Whenever ƒ(a 1 , . . . , a n ) is written, the function symbol ƒ is uninterpreted, and ƒ(a 1 , . . . , a n ) is then said to be uninterpreted. The procedure may be extended to allow interpreted function symbols from disjoint Shostak theories such as linear arithmetic and lists. The congruence closure procedure sets up the template for the extended procedure in Section 5.  
     [0057] The congruence closure decision procedure for pure equality has been studied by Kozen [Koz77], Shostak [Sho78], Nelson and Oppen [NO80], Downey, Sethi, and Tarjan [DST80], and, more recently, by Kapur [Kap97]. Presented here is the congruence closure algorithm in a Shostak-style, i.e., as an online algorithm for computing and using canonical forms by successively processing the input equations from the set T. For ease of presentation, use is made of variable abstraction in the style of the abstract congruence closure technique attributed to Bachmair, Tiwari, and Vigneron [BTV02]. Terms of the form ƒ(a 1 , . . . , a n ) are variable-abstracted into the form ƒ(x 1 , . . . , x n ) where the variables x 1 , . . . , x n  abstract the terms a 1 , . . . , a n , respectively. The procedure shown here can be seen as a specific strategy for applying the abstract congruence closure rules. In Section 5, essential use is made of variable abstraction in the Nelson-Oppen style where it is not merely a presentation device.  
     [0058] Let T={a 1 =b 1 , . . . , a n =b n } for n≧0 so that T is empty when n=0. Let x and y be metavariables that range over variables. The state of the algorithm consists of a solution state S and the input equalities T. The solution state S will be maintained as the pair (S V ; S U ), where (l 1 ; l 2 ; . . . ; l n ) represents a list with n elements and semi-colon is an associative separator for list elements. The set S U  then contains equalities of the form x=ƒ(x 1 , . . . , x n ) for an n-ary uninterpreted function ƒ, and the set S V  contains equalities of the form x=y between variables. The distinction is blurred between the equality a=b and the singleton set {a=b}. Syntactic identity is written as a≡b as opposed to semantic equality a=b.  
     [0059] A set of equalities R is functional if b≡c whenever a=b∈R and a=c∈R, for any a, b, and c. If R is functional, it can be used as a lookup table for obtaining the right-hand side entry corresponding to a left-hand side expression. Thus R(a)=b if a=bεR, and otherwise, R(a)=a. The domain of R, dom(R) is defined as {a|a=b∈R for some b}. When R is not necessarily functional, R({a}) is used to represent the set {b|a=b∈R b≡a} which is the image of {a} with respect to the reflexive closure of R. The inverse of R, written as R −1 , is the set {b=a |a=b∈R}. A functional set R of equalities can be applied as in R[a]. 
     
       R[x]=R[x] 
     
       R[ƒ ( a   1   , . . . , a   n )]= R (ƒ( R[a   1   ], . . . , R[a   n ])) 
       R[{a   1   =b   1   , . . . , a   n   =b   n   }]={R[a   1   ]=R[b   1   ], . . . , R[a   n   ]=R[b   n ]} 
     [0060] In typical usage, R will be a solution set where the left-hand sides are all variables, so that R[a] is just the result of applying R as a substitution to a.  
     [0061] When S V  is functional, then S given by (S V ; S U ) can also be used to compute the canonical form S[a] of a term a with respect to S. Hilbert&#39;s epsilon operator is used in the form of the when operator: F({overscore (x)}) when {overscore (x)}: P({overscore (x)}) is an abbreviation for F(ε{overscore (x)}: P({overscore (x)})), if ∃{overscore (x)}: P({overscore (x)}). 
       S[x]=S   V ( x ) 
       S[ƒ ( a   1   , . . . , a   n )]= S   V ( x ), when  x: x=ƒ ( S[a   1   ], . . . , S[a   n ])∈ S   U   
       S[ƒ ( a   1   , . . . , a   n )]=ƒ( S[a   1   ], . . . , S[a   n ]), otherwise. 
     [0062] The set S V  of variable equalities will be maintained so that vars(S V )∪vars(S U )=dom(S V ). The set S V  partitions the variables in dom(S V ) into equivalence classes. Two variables x and y are said to be in the same equivalence class with respect to S V  if S V (x)≡S V (y). If R and R′ are solution sets and R′ is functional, then R R′={a=R′[b]|a=b∈R}, and R∘R′=R′∪(R R′). The set S V  is maintained in idempotent form so that S V ∘S V =S V . Note that S U  need not be functional since it can, for example, simultaneously contain the equations x=ƒ(y), x=ƒ(z), and x=g(y).  
     [0063] Assume a strict total ordering x y on variables. The operation orient(x=y) returns {x=y} if x y, and returns {y=x}, otherwise. The solution state S is said to be congruence-closed if S U ({x})∩S U ({y})= whenever S V (x)≢S V (y). A solution set S is canonical if S is congruence-closed, S V  is functional and idempotent, and S U  is normalized, i.e., S U   S V =S U .  
     [0064] In order to determine if  (T├c=d), check if S′[c]≡S′[d] for S′ process(S;T), where S=(S V ;S U ), S V =id T , id T ={x=x|x∈vars(T)}, and S U =. The congruence closure procedure process is defined in Illustration 1.  
     [0065] Explanation. The congruence closure procedure is explained using the validity of the sequent ƒ(ƒ(ƒ(x)))=x, x=ƒ(ƒ(x))├ƒ(x)=x as an example. Its validity will be verified by constructing a solution state S′ equal to process(S V ; S U ; T) for T {ƒ(ƒ(ƒ(x)))=x, x=ƒ(ƒ(x))}, S V =id T , S U =, and checking S′[ƒ(x)]≡S′[x]. Note that id T  is (x=x). In processing ƒ(ƒ(ƒ(x)))=x with respect to S, the canonization step, S[ƒ(ƒ(ƒ(x)))=x] process(S;)=S  
     [0066] process(S; {a=b}∪T)=process(S′;T), where,  
     [0067] S′=close*(merge(abstract*(S;S[a=b]))).  
     [0068] close(S)=merge(S;S V (x)=S V (y)),  
     [0069] when x,y: S V (x)≢S V (y),(S U ({x})∩S U ({y})≠)  
     [0070] close(S)=S, otherwise.  
     [0071] merge(S;x=x)=S  
     [0072] merge(S;x=y)=(S′ V ;S′ U ), where x≢y,R=orient(x=y),  
     [0073] S′ V =S V ∘R,S′ U =S U   R.  
     [0074] abstract(S;x=y)=(S;x=y)  
     [0075] abstract(S;a=b)=(S′;a′=b′), when S′,a′, b′,x 1 , . . . , x n :  
     [0076] ƒ(x 1 , . . . , x n )∈[a=b] 
     [0077] x∈vars(S;a=b)  
     [0078] R=(x=ƒ(x 1 , . . . , x n )},  
     [0079] S′=(S V ∪{x=x}; S U ∪R),  
     [0080] a′=R −1 [a],b′=R −1 [b].  
     Illustration 1. Congruence Closure  
     [0081] yields ƒ(ƒ(ƒ(x)))=x, unchanged. Next, the variable abstraction step computes abstract*(ƒ(ƒ(ƒ(x)))=x). First ƒ(x) is abstracted to ν 1  yielding the state {x=x, ν 1 =ν 1 }; {ν 1 =ƒ(x)}; {ƒ(ƒ(ν 1 ))=x}. Variable abstraction eventually terminates renaming ƒ(ν 1 ) to ν 2  and ƒ(ν 2 ) to ν 3  so that S is {x=x, ν 1 =ν 1 , ν 2 =ν 2 , ν 3 =ν 3 }; {ν 1 =ƒf(x), ν 2 =ƒ(ν 1 ), ν 3 =ƒ(ν 2 )}. The variable abstracted input equality is then ν 3 =x. Let orient(ν 3 =x) return ν 3 =x. Next, merge(S; ν 3 =x) yields the solution state {x=x, ν 1 =ν 1 , ν 2 =ν 2 , ν 3 =x); {ν 1 =ƒ(x), ν 2 =ƒ(ν 1 ), ν 3 =ƒ(ν 2 )}. The congruence closure step close*(S) leaves S unchanged since there are no variables that are merged in S U  and not in S V .  
     [0082] The next input equality x=ƒ(ƒ(x)) is canonized as x=ν 2  which can be oriented as ν 2 =x and merged with S to yield the new value {x=x, ν 1 =ν 1 , ν 2 =x, ν 3 =x}; {ν 1 =ƒ(x), ν 2 =ƒ(ν 1 ), ν 3 =ƒ(x) for S. The congruence closure step close*(S) now detects that ν 1  and ν 3  are merged in S U  but not in S V  and generates the equality ν 1 =ν 3 . This equality is merged to yield the new value of S as {x=x, ν 1 =x, ν 2 =x, ν 3 =x}; {ν 1 =ƒ(x), ν 2 =ƒ(x), ν 3 =ƒ(x)}, which is congruence-closed.  
     [0083] With respect to this final value of the solution state S, it can be checked that S[ƒ(x)]≡x≡S[x].  
     [0084] Invariants. The Shostak-style congruence closure algorithm makes heavy use of canonical forms and this requires some key invariants to be preserved on the solution state S. If vars(S V ) ∪vars(S U ) ⊂ dom(S V ), then vars(S′ V ) ∪vars(S′ U ) ⊂ dom(S′ V ), when S′ is either abstract(S; a=b) or close(S). If S is canonical and a′=S[a], then S V [a′]=a′. If S U   S V =S U ,S V [a]=a, and S V [b]=b, then S′ U   S′ V =S′ U  where S′; a′=b′ is abstract(S; a=b). Similarly, if S U   S V =S U , S V (x)≡x, S V (y)≡y, then S′ U ∘S′ V =S′ U  for S′=merge(S; x=y). If S V  is functional and idempotent, then so is S′ V , where S′ is either of abstract(S; a=b) or close(S). If S′=close*(S), then S′ is congruence-closed, and if S V  is functional and idempotent, S U  is normalized, then S′ is canonical.  
     [0085] Variations. In the merge operation, if S′ U  is computed as R[S U ]instead of S U   R, then this would preserve the invariant that S U   −1  is always functional and S V [S U ]=S U . If this is the case, the canonizer can be simplified to just return S U   −1 (ƒ(S[a 1 ], . . . , S[a n ])).  
     [0086] Termination. The procedure process(S; T) terminates after each equality in T has been asserted into S. The operation abstract* terminates because each recursive call decreases the number of occurrences of function applications in the given equality a=b by at least one. The operation close* terminates because each invocation of the merge operation merges two distinct equivalence classes of variables in S V . The process operation terminates because the number of input equations in T decreases with each recursive call. Therefore the computation of process(S; T) terminates returning a canonical solution set S.  
     [0087] Soundness and Completeness. It is necessary to show that  (T├c=d) S′[c]≡S′[d] for S′=process(id T ; ; T) and vars(c=d) ⊂ vars(T). This is done by showing that S′ preserves (id T   ; ; T), and hence  (T├c=d)   (S′├c=d), and  (S′├c=d) S′[c]≡S′[d]. It can easily be established that if process(S; T)=S′, then S′ preserves (S; T). If a′=b′ is obtained from a=b by applying equality replacements from S, then (S; a′=b′) preserves (S; a=b). In particular,  (S├S[c]=c) holds. The following claims can then be easily verified.    
     [0088] 1. (S; S[a=b] preserves (S;a=b).  
     [0089] 2. abstract(S;a=b) preserves (S;a=b).  
     [0090] 3. merge(S;a=b) preserves (S;a=b).  
     [0091] 4. close(S) preserves S.  
     [0092] The only remaining step is to show that if S′ is canonical, then  (S′├c=d) S′[c]≡S′[d] for vars(c=d) ⊂ vars(S). Since it is known that  S′├S′[c]=c and  S′├S′[d]=d, hence  (S′├c=d) follows from S′[c]≡S′[d]. For the only if direction, it is shown that if S′[c]≢S′[d], then there is an interpretation M S′  and assignment ρ S′  such that M S′ , ρ S′   S but M S′ , ρ S′   c=d. A canonical term (in S′) is a term a such that S′[a]≡a. The domain D S′  is taken to be the set of canonical terms built from the function symbols F and variables from vars(S′). Constrain M S′  so that M S′ (ƒ)(a 1 , . . . , a n )=S′ V (x) when there is an x such that x=ƒ(a 1 , . . . , a n )εS′ U , and ƒ(a 1 , . . . , a n ), otherwise. Let ρ S′  map x in vars(S′) to S′ V (x); the mappings for the variables outside vars(S′) are irrelevant. It is easy to see that M S′ [c]ρ S′ =S′[c] by induction on the structure of c. In particular, when S′ is canonical, M S′ (ƒ)(x 1 , . . . , x n )=x for ƒ(x 1 , . . . , x n )εS′ U , so that one can easily verify that M S′ , ρ S′   S′. Hence, if S′[c]≢S′[d], then  (S′├c=d).  
     [0093] 4 Shostak Theories  
     [0094] A Shostak theory [Sho84] is a theory that is canonizable and solvable. Assume a collection of Shostak theories θ 1 , . . . , θ N . In this section, decision procedure is given for a single Shostak theory θ i , but with i as a parameter. This background material is adapted from Shankar [Sha01]. Satisfiability M, ρ a=b is with respect to i-models M. The equality a=b is i-valid, i.e.,    i a=b, if for all i-models M and assignments ρ, M[a]ρ=M[b]ρ. Similarly, a=b is i-unsatisfiable, i.e.,    i a≠b, when for all i-models M and assignments ρ, M[a]≠M[b]ρ. An i-term a is a term whose function symbols all belong to θ i  and vars(a) ⊂ X∪X i .  
     [0095] A canonizable theory θ i  admits a computable operation σ i  on terms such that    i a=b iff σ i (a)≡σ i (b), for i-terms a and b. An i-term a is canonical if σ i (a)≡a. Additionally, vars(σ i (a)) ⊂ vars(a) and every subterm of σ i (a) must be canonical. For example, a canonizer for the theory θ A  of linear arithmetic can be defined to convert expressions into an ordered sum-of-monomials form. Then, σ A (y+x+x)≡2*x+y≡σ A (x+y+x).  
     [0096] A solvable theory admits a procedure solve i  on equalities such that solve i (Y)(a=b) for a set of variables Y with vars(a=b) ⊂ Y, returns a solved form for a=b as explained below. solve i (Y)(a=b) might contain fresh variables that do not appear in Y. A functional solution set R is in i-solved form if it is of the form {x 1 =t 1 , . . . , x n =t n }, where for j, 1≦j≦n, t j  is a canonical i-term, σ i (t j )≡t j , and vars(t j )∩dom(R)= unless t j ≡x j . The i-solved form solve i (Y)(a=b) is either ⊥ i , when    i a≠b, or is a solution set of equalities which is the union of sets R 1  and R 2 . The set R 1  is the solved form {x 1 =t 1 , . . . , x n =t n } with x j ∈vars(a=b) for 1≦j≦n, and for any i-model M and assignment ρ, M,ρ a=b iff there is a ρ′ extending ρ over vars(solve i (Y)(a=b))−Y such that M,ρ′ x j =t j , for 1≦j≦n. The set R 2  is just {x=x|x∈vars(R 1 )−Y} and is included in order to preserve variables. In other words, solve i (Y)(a=b) i-preserves a=b. For example, a solver for linear arithmetic can be constructed to isolate a variable on one side of the equality through scaling and cancellation. Assume that the fresh variables generated by solve i  are from the set X i . Take vars(⊥ i ) to be X∪X i , so as to maintain variable preservation, and indeed ⊥ i  could be represented as just ⊥ were it not for this condition.  
     [0097] A decision procedure is described for sequents of the form T├c=d in a single Shostak theory with canonizer σ i  and solver solve i . Here the solution state S is just a functional solution set of equalities in i-solved form. Given a solution set S, define S&lt;&lt;a&gt;&gt; i  as σ i (S[a]). The composition of solutions sets is defined so that S∘ i ⊥ i =⊥ i ∘ i S=⊥ i  and S∘ i R=R∪{a=R&lt;&lt;b&gt;&gt; i |a=b∈S}. Note that solved forms are idempotent with respect to composition so that S∘ i  S=S. The solved form solveclose i (id T ; T) is obtained by processing the equations in T to build up a solution set S. An equation a=b is first canonized with respect to S as S&lt;&lt;a&gt;&gt; i =S&lt;&lt;b&gt;&gt; i  and then solved to yield the solution R. If R is ⊥ i , then T is i-unsatisfiable and one returns the solution state with S i =⊥ i  as the result. Otherwise, the composition S∘ i R is computed and used to similarly process the remaining formulas in T.  
     [0098] solveclose i (S; )=S  
     [0099] solveclose i (⊥ i ; T)=⊥ i    
     [0100] solveclose i (S; {a=b}∪T=solveclose i (S′,T),  
     [0101] where S′=S∘ i  solve i (vars(S))(S&lt;&lt;a&gt;&gt; i =S&lt;&lt;b&gt;&gt; i )  
     [0102] To check i-validity,    i (T├c=d), it is sufficient to check that either  
     [0103] solveclose i (id T ; T)=⊥ or S′&lt;&lt;c&gt;&gt; i ≡S′&lt;&lt;d&gt;&gt; i , where S′=solveclose i (id T ; T).  
     [0104] Soundness and Completeness. As with the congruence closure procedure, each step in solveclose i  is i-conservative. Hence solveclose i is sound and complete: if S′=solveclose i (S; T), then for every i-model M and assignment ρ, M, ρ S∪T iff there is a ρ′ extending ρ over the variables in vars(S′)−vars(S) such that M,ρ′ S′. If σ i (S′[a])≡σ i (S′[b]), then M,ρ′ a=S′[a]=σ i (S′[a])=σ i (S′[b])=S′[b]=b, and hence M, ρ a=b. Otherwise, when σ i (S′[a])≢σ i (S′[b]), it is known by the condition on σ i  that there is an i-model M and an assignment ρ′ such that M[S′[a]]ρ′≠M[S′[b]]ρ′. The solved form S′ divides the variables into independent variables x such that S′(x)=x, and dependent variables y where y≠S′(y) and the variables in vars(S′(y)) are all independent. One can therefore extend ρ′ to an assignment ρ where the dependent variables y are mapped to M[S′(y)]ρ′. Clearly, M,ρ S′, M,ρ a=S′[a], and M,ρ b=S′[b]. Since S′ i-preserves (id T ; T), M,ρ T but M,ρ a=b and hence T├a=b is not i-valid, so the procedure is complete. The correctness argument is thus similar to that of Section 3 but for the case of a single Shostak theory considered here, there is no need to construct a canonical term model since    i  a=σ i (a), and σ i (a)≡σ i (b) iff    i a=b.  
     [0105] Canonical term model. The situation is different when one wishes to combine Shostak theories. It is important to resolve potential semantic incompatibilities between two Shostak theories. With respect to some fixed notion of i-validity for θ i  and j-validity for θ j  with i≠j, a formula A in the union of θ i  and θ j  may be satisfiable in an i-interpretation of only a specific finite cardinality for which there might be no corresponding satisfying j-interpretation for the formula. Such an incompatibility can arise even when a theory θ i  is extended with uninterpreted function symbols. For example, if φ is a formula with variables x and y that is satisfiable only in a two-element model M where ρ(x)≠ρ(y), then the set of formulas Γ where Γ=(φ,ƒ(x)=x, ƒ(u)=y, ƒ(y)=x} additionally requires ρ(x)≠ρ(u) and ρ(y)≠ρ(u). Hence, a model for Γ must have at least three elements, so that Γ is unsatisfiable. However there is no way to detect this kind of unsatisfiability purely through the use of solving and canonization.  
     [0106] A canonical term model is introduced as a way around such semantic incompatibilities. The set of canonical i-terms a such that σ i (a)≡a yields a domain for a term model M i  where M i (ƒ)(a 1 , . . . , a n )=σ i (ƒ(a 1 , . . . , a n ). If M i  is (isomorphic to) an i-model, then the theory θ i  is composable. Note that the solve operation is conservative with respect to the model M i  as well, since M i  is taken as an i-model.  
     [0107] Given the usual interpretation of disjunction, a notion of validity is said to be convex when  (T├c 1 =d 1     . . .   c n =d n ) implies  (T├c k   32  d k ) for some k, 1≦k≦n. If a theory θ i  is composable, then i-validity is convex. Recall that  , i(T├c 1 =d 1     . . .   c n =d n ) iff    i (S├c 1 =d 1     . . .   c n =d n ) for S solveclose i (id T ; T). If S≠⊥ i , then    i (T├c k =d k ), for 1≦k≦n. If S≠⊥ i , then since S i-preserves T,   i (S├c 1 =d 1     . . .   c n =d n ), but (by assumption)    i (S├c k   32  d k ). An assignment ρ S  can be constructed so that for independent (i.e., where S(x)=x) variables xεvars(S), ρ S (x)=x, and for dependent variables y∈vars(S), ρ S (y)=M i [S(y)]ρ S . If for S≠⊥ i ,    σ , (S├c k =d k ), then M i , σ S   c k   32  d k . Hence M i , ρ S   (S├c k =d k ), for 1≦k≦n. This yields M i ,ρ S   (T├c 1 =d 1     . . .   c n =d n ), contradicting the assumption.  
     [0108] 5 Combining Shostak Theories  
     [0109] The combination of the theory of equality over uninterpreted function symbols with several disjoint Shostak theories is now examined. Examples of interpreted operations from Shostak theories include + and − from the theory of linear arithmetic, select and update from the theory of arrays, and cons, car, and cdr from the theory of lists. The basic Shostak combination algorithm covers the union of equality over uninterpreted function symbols and a single canonizable and solvable equational theory [Sho84, CLS96, RS01]. Shostak [Sho84] had claimed that the basic combination algorithm was sufficient because canonizers and solvers for disjoint theories could be combined into a single canonizer and solver for their union. This claim is incorrect.  3  A combined decision procedure for multiple Shostak theories is presented that overcomes the difficulty of combining solvers.  
     [0110] Two theories θ 1  and θ 2  are said to be disjoint if they have no function symbols in common. A typical subgoal in a proof can involve interpreted symbols from several theories. Let σ i  be the canonizer for θ i . A term ƒ(a 1 , . . . , a n ) is said to be in θ i  if ƒ is in θ i  even though some a i  might contain function symbols outside θ i . In processing terms from the union of pairwise disjoint theories θ 1 , . . . , θ N , it is quite easy to combine the canonizers so that each theory treats terms in the other theory as variables. Since σ i  is only applicable to i-terms, one first has to extend the canonizer σ i  to treat terms in θ j  for j≠i, as variables. Treat uninterpreted function symbols as belonging to a special theory θ 0  where σ 0 (a)=a for aεθ 0 . The extended operation σ′ i  is defined below.  
     [0111] σ′ i (a)=R[σ i (a′)], when a′,b,R a′ is an i-term,  
     [0112] R is functional,  
     [0113] dom(R) ⊂ vars(a′),  
     [0114] R(x)εθ j , for x∈dom (R), some j≠i,  
     [0115] R[a′]≡a  
     [0116] Note that the when condition in the above definition can always be satisfied. The combined canonizer σ can then be defined as  
     [0117] σ(x)=x  
     [0118] σ(ƒ(a 1 , . . . , a n ))=σ′ i (ƒ(σ(a 1 ), . . . , σ(a n ))), when i: ƒ is in θ i .  
     [0119] A discussion of the difficulty of combining the solvers solve 1  and solve 2  for θ 1  and θ 2 , respectively, into a single solver follows. The example uses the theory θ A  of linear arithmetic and the theory θ L  of the pairing and projection operations cons, car, cdr, where, somewhat nonsensically, the projection operations also apply to numerical expressions. Shostak illustrated the combination using the example  
     [0120] 5+car(x+2)=cdr(x+1)+3.  
     [0121] Since the top-level operation on the left-hand side is +, car(x+2) and cdr(x+1) are treated as variables and use solve A . This might yield a partially solved equation of the form car(x+2)=cdr(x+1)−2. Now because the top-level operation on the left-hand side is from the theory of lists, use solve L , to obtain x+2=cons(cdr(x+1)−2, u) with a fresh variable u. Once again apply solve A  to obtain x=cons(cdr(x+1)−2, u)−2. This is, however, not in solved form: the left-hand side variable occurs in an interpreted context in its solution. There is no way to prevent this from happening as long as each solver treats terms from another theory as variables. Therefore the union of Shostak theories is not necessarily a Shostak theory.  
     [0122] The problem of combining disjoint Shostak theories actually has a very simple solution. There is no need to combine solvers. Since the theories are disjoint, the canonizer can tolerate multiple solutions for the same variable as long as there is at most one solution from any individual theory. This can be illustrated on the same example: 5+car(x+2)=cdr(x+1)+3. By variable abstraction, one obtains the equation ν 3 =ν 6 , where ν 1 =x+2, ν 2 =car(ν 1 ), ν 3 =ν 2 +5, ν 4 =x+1, ν S =cdr(ν 4 ), ν 6 =ν 5 +3. One can separate these equations out into the respective theories so that S is (S V ; S U ; S A ; S L ), where S V  contains the variable equalities in canonical form, S U  is as in congruence closure but is always  since there are no uninterpreted operations in this example, and S A  and S L , are the solution sets for θ A  and θ L , respectively. One then gets S V ={x=x, ν 1 =ν 1 , ν 2 =ν 2 , ν 3 =ν 6 , ν 4 =ν 4 , ν 5 =ν 5 , ν 6 =ν 6 }, S A ={ν 1 =x+2, ν 3 =ν 2 +5, ν 4 =x+1, ν 6 =ν 5 +3}, and S L ={ν 2 =car(ν 1 ), ν 5 =cdr(ν 4 )}. Since ν 3  an ν 6  are merged in S V , but not in S A , solve the equality between S A (ν 3 ) and S A (ν 6 ), i.e., solve A (ν 2 +5=ν 5 +3) to get ν 2 =ν 5 −2. This result is composed with S A  to get {ν 1 =x+2, ν 3 =ν 5 +3, ν 4 =x+1, ν 6 =ν 5 +3, ν 2 =ν 5 − 2 } for S A . There are no new variable equalities to be propagated out of either S A , S L , or S V . Notice that ν 2  and ν 5  both have different solved forms in S A  and S L . This is tolerated since the solutions are from disjoint theories and the canonizer can pick a solution that is appropriate to the context. For example, when canonizing a term of the form ƒ(x) for ƒεθ i , it is clear that the only relevant solution for x is the one from S i .  
     [0123] It may now be checked whether the resulting solution state verifies the original equation 5+car(x+2)=cdr(x+1)+3. In canonizing ƒ(a 1 , . . . , a n ) return S V (y) whenever the term ƒ(S i (S[a 1 ], . . . , S i (S[a n ])) being canonized is such that y=ƒ(S i (S[a 1 ], . . . , S i (S[a n ]))∈S i  for ƒ∈θ i . Thus x+2 canonizes to ν i  using S A , and car(ν 1 ) canonizes to ν 2  using S L . The resulting term 5+ν 2 , using the solution for ν 2  from S A , simplifies to ν 5 +3, which returns the canonical form ν 6  by using S A . On the right-hand side, x+1 is equivalent to ν 4  in S A , and car(ν 4 ) simplifies to ν 5  using S L . The right-hand side therefore simplifies to ν 5 +3 which is canonized to ν 6  using S A . The canonized left-hand and right-hand sides are identical.  
     [0124] A formal description of the procedure used informally in the above example is presented, showing how process from Section 3 can be extended to combine the union of disjoint solvable, canonizable, composable theories. Assume that there are N disjoint theories θ 1 , . . . , θ N . Each theory θ i  is equipped with a canonizer σ 1  and solver solve i  for i-terms. If I represents the interval [1, N], then an I-model is a model M that is an i-model for each i∈I. This will ensure that each inference step is conservative with respect to I-models, i.e., I-conservative. Represent the uninterpreted part of S as S 0  instead of S U . The solution state S of the algorithm now consists of a list of sets of equations (S V ; S 0 ; S 1 ; . . . ; S N ). Here S V  is a set of variable equations of the form x=y, and S 0  is the set of equations of the form x=ƒ(x 1 , . . . ,x n ) where ƒ is uninterpreted. Each S i  is in i-solved form and is the solution set for θ i .  
     [0125] Terms now contain a mixture of function symbols that are uninterpreted or are interpreted in one of the theories θ i . A solution state S is confluent if for all x, y∈dom(S V ) and i, 0≦i≦N: S V (x)≡S V (y) S i ({x})∩S i ({y})≠. A solution state S is canonical if it is confluent; S V  is functional and idempotent, i.e., S V ∘S V =S V ; the uninterpreted solution set S 0  is normalized, i.e., S 0   S V =S 0 ; each S i , for i&gt;0, is functional, idempotent, i.e., S i ∘ i S i =S i , normalized i.e., S i   S V =S i , and in i-solved form. The canonization of expressions with respect to a canonical solution set S is defined as follows.  
     [0126] S[x]=S V (x)  
     [0127] abstract(S; x=y)=(S; x=y),  
     [0128] abstract(S; a=b)=(S′; a′=b′),  
     [0129] when S′,c,i: c∈max([a=b],),  
     [0130] x∉vars(S∪a=b),  
     [0131] S′ V =S V ∪{x=x},  
     [0132] S′ i =S i ∪{x=c},  
     [0133] S′ j =S j , for, i≠j  
     [0134] a′={C=x}[a],  
     [0135] b′={c=x}[b].  
     Illustration 2. Variable Abstraction Step for Multiple Shostak Theories  
     [0136] S [ƒ(a 1 , . . . , a n )]=S V (x), when i,x:  
     [0137] i≧0,ƒ∈θ i ,x=σ′ i ,(ƒ(S i (S[a 1 ]), . . . , S i (S[a n ])))∈S i    
     [0138] S[ƒ(a 1 , . . . , a n )]=σ′ i (ƒ(S i (S[a 1 ]), . . . , S i (S[a n ]))), when i: ƒεθ i ,i≧0.  
     [0139] Since variables are used to communicate between the different theories, the canonical variable x in S V  is returned when the term being canonized is known to be equivalent to an expression a such that y=a in S i , where x≡S V (y). The definition of the above global canonizer is an important aspect of the invention. This definition can be applied to the example above of computing S[5+car(x+2)].  
     [0140] Variable Abstraction. The variable abstraction procedure abstract(S; a=b) is shown in Illustration 2. If a is an i-term such that a∉X, then a is said to be a pure i-term. Let [a=b] i  represent the set of subterms of a=b that are pure i-terms. The set max(M) of maximal terms in M is defined to be {a∈M|a≡b   a∉[b], for any b ∈M}. In a single variable abstraction step, abstract(S; a=b) picks a maximal pure i-subterm c from the canonized input equality a=b, and replaces it with a fresh variable x from X while adding x=c to S i . By abstracting a maximal pure i-term, it is ensured that S i  remains in i-solved form.  
     [0141] Explanation. The procedure in Illustration 3 is similar to that of Illustration 1. Equations from the input set T are processed into the solution state S of the form S V ; S 0 ; . . . ; S N . Initially, S must be canonical. In processing the input equation a=b into S, steps are taken to systematically restore the canonicity of S. The first step is to compute the canonical form S[a=b] of a=b with respect to S. It is easy to see that (S; S[a=b]) I-preserves (S; a=b).  
     [0142] The result of the canonization step a′=b′ is then variable abstracted as abstract*(a′=b′) (shown in Illustration 2) so that in each step, a maximal, pure i-subterm c of a′=b′ is replaced by a fresh variable x, and the equality x=c is added to S i . This is also easily seen to be an I-conservative step. The equality x=y resulting from the variable abstraction of a′=b′ is then merged into S V    
     [0143] process(S; )=S  
     [0144] process(S; T)=S, when i: S i=⊥   i    
     [0145] process(S; {a=b}∪T=process(S′; T), where  
     [0146] S′=close*(merge V (abstract*(S; S[a=b]))).  
     [0147] close(S)=S, when i: S i =⊥ i    
     [0148] close(S)=S′, when S′,i, x,y:  
     [0149] x,y∈dom(S V ),  
     [0150] (i&gt;0, S V (x)≡S V (y), S i (x)≢S i (y), and  
     [0151] S′=merge i (S; x=y)) or  
     [0152] (i≧0,S V (x)≢S V (y)S i ({x}))∪S i ([y])≠, and  
     [0153] S′=merge V (S; S V (x)=S V (y)))  
     [0154] close(S)=normalize(S), otherwise.  
     [0155] normalize(S)=(S V ; S O ; S 1    S V ; . . . ; S N   S V ).  
     [0156] merge i (S;x=y)=S′, where i&gt;0,  
     [0157] S′ i =S i ∘ i  solve i (vars(S i ))(S i (x)=S i (y)),  
     [0158] S′ j =S j , for i≠j,  
     [0159] S V =S V .  
     [0160] merge V (S; x=x)=S  
     [0161] merge V (S; x=y)=(S V ∘R; S O    R; S 1 ; . . . ; S N ), where R=orient(x=y).  
     Illustration 3. Combining Multiple Shostak Theories  
     [0162] and S 0 . This can destroy confluence since there may be variables w and z such that w and z are merged in S V  (i.e., S V (w)≡S V (z)) that are unmerged in some S i  (i.e., S i ({w})∩S i ({z})=), or vice-versa. 4  The number of variables in dom(S V ) remains fixed during the computation of close*(S). Confluence is restored by close*(S) which finds a pair of variables that are merged in some S i  but not in S V , and merging them in S V , or that are merged in S V  and not in some S i  and merging them in S i . Each such merge step is also I-conservative. When this process terminates, S is once again canonical. The solution sets S i  are normalized with respect to S V  in order to ensure that the entries are in the normalized form for lookup during canonization.  
     [0163] Invariants. As with congruence closure, several key invariants are needed to ensure that the solution state S is maintained in canonical form whenever it is given as the argument to process. If S is canonical and a and b are canonical with respect to S, then for (S′; a′=b′)=abstract(S; a=b), S′ is canonical, and a′ and b′ are canonical with respect to S′. The state abstract(S; a=b) I-preserves (S; a=b). A solution state is said to be well-formed if S V  is functional and idempotent, S 0  is normalized, and each S i  is functional, idempotent, and in solved form. Note that if S is well-formed, confluent, and each S i , is normalized, then it is canonical. When S is well-formed, and S′=merge V (S; x=y) or S′=merge i (S; x=y), then S′ is well-formed and I-preserves (S; x=y). If S is well-formed and congruence-closed, and S′=normalize(S), then S′ is well-formed and each S′ i  is normalized. If S′=normalize(S), then each S′ i  is in solved form because if x replaces y on the right-hand side of a solution set S i , then S i (y)≡y since S i  is in i-solved form. By congruence closure, S i (x)≡S i (y)≡y. Therefore, the uniform replacement of y by x ensures that S′ i (x)≡x, thus leaving S in solved form. If S′=close*(S), where S is well-formed, then S′ is canonical.  
     [0164] Variations. As with congruence closure, once S is confluent, it is safe to strengthen the normalization step to replace each S i  by S V [S i ]. This renders S o   −1  functional, but S i   −1  may still be non-functional for i&gt;0, since it might contain left-hand side variables that are local. However, if S i  is taken to be S i  restricted to dom(S V ), then S i   −1  with the strengthened normalization is functional and can be used in canonization. The solutions for local variables can be safely discarded in an actual implementation. The canonization and variable abstraction steps can be combined within a single recursion.  
     [0165] Termination. The operations S[a=b] and abstract*(S; a=b) are easily seen to be terminating. The operation close*(S) also terminates because the sum of the number of equivalence classes of variables in dom(S V ) with respect to each of the solution sets S V , S 0 , S 1 , . . . , S N , decreases with each merge operation.  
     [0166] Soundness and Completeness. It has already been seen that each of the steps: canonization, variable abstraction, composition, merging, and normalization, is I-conservative. It therefore follows that if S′=process(S; T), then S′ I-preserves S. Hence, if S′[c]≡S′[d], then clearly    1 (S′├c=d), and hence    1 (S; T├c=d).  
     [0167] The completeness argument requires the demonstration that if S′[c]≢S′[d], then    1 (S′├c=d) when S′ is canonical. This is done by means of a construction of M S′ and ρ S′ , such that M S′ , ρ S′   S′ but M S′ , ρ S′   c=d. The domain D consists of canonical terms e such that S′[e]=e. As with congruence closure, M S′  is defined so that M S′ (ƒ)(e 1 , . . . , e n .)=S′[ƒ(e 1 , . . . , e n )]. The assignment ρ S  is defined so that ρ S′ (x)=S V (x). By induction on c, M S′ [c]ρ S′ =S′[c]. One may easily check that M S′ , ρ S′   S′.  
     [0168] It is also the case that M S′  is an I-model since M S′  is isomorphic to M i  for each i, 1≦i≦N. This can be demonstrated by constructing a bijective map μ i  between D and the domain D i  corresponding to M i . Let P i  be the set of pure I-terms in D, and let γ be a bijection between D−P i  and X such that γ(x)=x if S′ i (x)=x for x∈dom(S′ V ). Define μ i  so that μ i (x)=S′ i (x) for x∈dom(S′ V ) and S′ V (x)=x, μ i (y)=y for y∈X i , μ i  (ƒ(a 1 , . . . , a n ))=ƒ(μ i  (a 1 ), . . . , μ i (a n )) for ƒεθ i , and μ i (a)=γ(a), otherwise. It can then be verified that for an i-term a, μ i (M S′ [a]ρ)=M i [a]ρ i , where ρ i (x)=μ i (ρ(x)). This concludes the proof of completeness.  
     [0169] Convexity revisited. As in Section 4, the term model construction of M S′  once again establishes that I-validity is convex. In other words, a sequent    1 (T├c 1 =d 1 V . . . V c n =d n ) iƒƒ    1 (T├c k   32  d k ) for some k, 1≦k≦n.  
     [0170] Ground decision procedures for equality are crucial for discharging the myriad proof obligations that arise in numerous applications of automated reasoning. These goals typically contain operations from a combination of theories, including uninterpreted symbols. Shostak&#39;s basic method deals only with the combination of a single canonizable, solvable theory with equality over uninterpreted function symbols. Indeed, in all previous work based on Shostak&#39;s method, only the basic combination is considered. Though Shostak asserted that the basic combination was adequate to cover the more general case of multiple Shostak theories, this claim has turned out to be false. Given here is the first Shostak-style combination method for the general case of multiple Shostak theories.  
     [0171] The inventive method, in the embodiment described herein, is clearly an instance of a Nelson-Oppen combination [N079] because it involves the exchange of equalities between variables through the solution set S V , but with the added advantage of a Shostak combination in that it combines the canonizers of the individual theories into a global canonizer. The definition of such a canonizer for multiple Shostak theories is unique to the inventive method. The technique of achieving confluence across the different solution sets is also unique to the inventive method. Confluence is needed for obtaining useful canonical forms, and is therefore not essential in a general Nelson-Oppen combination. The global canonizer S[a] can be applied to input formulas to discharge queries and simplify input formulas. The reduction to canonical form with respect to the given equalities helps keep the size of the term universe small, and makes the algorithm more efficient than a black box Nelson-Oppen combination. The decision algorithm for a Shostak theory given in Section 4 fits the requirements for a black box procedure that can be used within a Nelson-Oppen combination. The Nelson-Oppen combination of Shostak theories with other decision procedures has been studied by Tiwari [Tiw00], Barrett, Dill, and Stump [BDS02], and Ganzinger [Gan02], but none of these methods includes a general canonization procedure as is required for a Shostak combination.  
     [0172] Variable abstraction is also used in the combination unification procedure of Baader and Schulz [BS96], which addresses a similar problem to that of combining Shostak solvers. In the inventive method, there is no need to ensure that solutions are compatible across distinct theories. Furthermore, variable dependencies can be cyclic across theories so that it is possible to have y∈vars(S i (x)) and x∈vars(S j (y)) for i≠j. The inventive algorithm can be easily and usefully adapted for combining unification and matching algorithms with constraint solving in Shostak theories.  
     [0173] Insights derived from the Nelson-Oppen combination method have been crucial in the design of the inventive algorithm and its proof. Proof of the basic algorithm additionally demonstrated the existence of proof objects in a sound and complete proof system [RS01]. This can easily be replicated for the embodiment of the general algorithm described herein. The soundness and completeness proofs given herein are for composable theories and avoid the use of σ-models.  
     [0174] The inventive Shostak-style algorithm fits modularly within the Nelson-Oppen framework. It can be employed within a Nelson-Oppen combination in which there are other decision procedures that generate equalities between variables. It is also possible to combine it with decision procedures that are not disjoint, as for example with linear arithmetic inequalities. Here, the existence of a canonizer with respect to equality is useful for representing inequality information in a canonical form. A variant of the procedure described here has been reduced to practice in ICS™ (a software product of the assignee of the present invention) [FORS01] in exactly such a combination.  
     [0175] It will be appreciated that the preferred embodiments described above are cited by way of example, and that the invention is not limited to what has been particularly shown and described hereinabove. Rather, the scope of the invention includes both combinations and subcombinations of the various features described hereinabove, as well as variations and modifications thereof not disclosed in the prior art and which would occur to persons skilled in the art upon reading the foregoing description.