OrderSorted Rewriting and Congruence Closure
 429 Downloads
Abstract
Ordersorted type systems supporting inheritance hierarchies and subtype polymorphism are used in theorem proving, AI, and declarative programming. The satisfiability problems for the theories of: (i) ordersorted uninterpreted function symbols, and (ii) of such symbols modulo a subset \(\varDelta \) of associativecommutative ones are reduced to the unsorted versions of such problems at no extra computational cost. New results on ordersorted rewriting are needed to achieve this reduction.
Keywords
Ordersorted rewriting Congruence closure Satisfiability1 Introduction
For greater expressiveness and efficiency, type systems supporting inheritance hierarchies and subtype polymorphism are used in many areas such as resolution theorem proving, e.g., [26, 32], declarative logic and rulebased languages, e.g., [4, 9, 10, 29], and artificial intelligence, e.g., [8, 29]. Ordersorted (OS) equational logic, e.g., [15, 21], is a logical framework supporting inheritance hierarchies and subtype polymorphism widely used for these purposes. Therefore, the development of decision procedures for OS theories is of interest in all these areas. I focus here on decision procedures for the OS theory of uninterpreted function symbols, which in an unsorted setting is decided by congruence closure algorithms [7, 24, 27]. However, for greater expressiveness one can allow some of the function symbols, say in a subsignature \(\varDelta \subseteq \varSigma \), to be interpreted by some axioms \(B_{\varDelta }\). For example, for an unsorted subsignature \(\varDelta \subseteq \varSigma \) of binary function symbols, congruence closure algorithms modulo the axioms \(AC_{\varDelta }\), asserting the associativity and commutativity of all symbols in \(\varDelta \) have been given in [2, 19, 22]. Therefore, I also study satisfiability in the OS theory \((\varSigma ,AC_{\varDelta })\) of uninterpreted function symbols\(\varSigma \)modulo\(AC_{\varDelta }\).
The most obvious approach would be to develop an ordersorted congruence closure algorithm along the lines of [11] and then extended it to the modulo AC case. However, the main, somewhat surprising message of this paper is that such OS congruence closure algorithms are not needed at all: the already existing and efficient unsorted congruence closure algorithms in [7, 24, 27] and congruence closure modulo \(AC_{\varDelta }\) in [2, 19, 22] and tools supporting them can be reused without change and at no extra cost to solve the corresponding OS satisfiability problems.
A Simple Example. Consider the following ordersorted signature \(\varSigma \)
An approach using rewriting \([\ldots ]\) fails due to the wellknown problem that rewriting with ordersorted rewrite rules may create illtyped terms.
Let us now widen the problem into one of satisfiability moduloAC by making the \(+\) symbol associativecommutative. That is, we consider the axioms \( AC _{+}=\{x+y=y+x,(x+y)+z=x+(y+z)\}\), with x, y, z of sort A, and ask: is the formula \((\flat )\)\((\varSigma , AC _{+})\)satisfiable? For this case, I am not aware of any ordersorted ACcongruence closure algorithm, but unsorted, groundACcompletionbased ones exist [2, 19, 22]. The trouble, again, is that ordersortedACcompletion as in [13] fails miserably in the same way (\(a=c\) cannot be oriented).
Wouldn’t it be nice if we could completely ignore all sort information in the above two OS satisfiability problems and solve them as unsorted problems using standard (and efficient!) congruence closure [7, 24, 27] and congruence closure modulo AC [2, 19, 22] algorithms? If this reduction method were sound, we could easily settle the \((\varSigma ,\emptyset )\) and \((\varSigma , AC _{+})\)satisfiability of \((\flat )\): the confluent and terminating rules \(R=\{a \rightarrow b, c \rightarrow b,f(f(b)) \rightarrow f(b)\}\) play the role of a “congruence closure” for the first three equations, and also of an \(AC_{+}\)congruence closure. Since the disequality \( a+f(f(a)) \not = f(a)+a\) reduces to \( b+f(b) \not = f(b)+b\), the formula \((\flat )\) is \((\varSigma ,\emptyset )\)satisfiable. However, since \( b+f(b) =_{AC_{+}} f(b)+b\), \((\flat )\) is \((\varSigma , AC _{+})\)unsatisfiable. But is this reduction to unsorted satisfiability sound?
Initial Algebra Semantics of Uninterpreted Satisfiability. Ignoring the sort information of an OS signature \(\varSigma \) is captured by a signature map \(u: \varSigma \ni (f: s_{1} \ldots s_{n} \rightarrow s) \mapsto (f: U \mathop {\ldots }\limits ^{n} U \rightarrow U) \in \varSigma ^{u}\), where U is the single “universe” sort in the unsorted signature \(\varSigma ^{u}\). As further detailed at the end of Sect. 2, u induces a reduct map of algebras in the opposite direction, \(\__{u}: \mathbf{Alg}_{\varSigma ^{u}} \ni A \mapsto A_{u} \in \mathbf{OSAlg}_{\varSigma }\), making each unsorted algebra A into and ordersorted one \(A_{u}\), and such that for a set of ground OS \(\varSigma \)equations E we have the equivalence: \(A_{u}\models E \; \Leftrightarrow \; A \models E\). In particular, the Einitial unsorted \(\varSigma ^{u}\)algebra \(T_{\varSigma ^{u}/E}\) is mapped to the OS \(\varSigma \)algebra \(T_{\varSigma ^{u}/E}_{u}\) and, since \(T_{\varSigma ^{u}/E}_{u}\models E\), there is a unique OS homomorphism \(h:T_{\varSigma /E} \rightarrow T_{\varSigma ^{u}/E}_{u}\) from the Einitial OS \(\varSigma \)algebra \(T_{\varSigma /E}\).
But the proof of Theorem 5 shows that, for equations E and disequations D, the conjunction \(\bigwedge E \, \wedge \, \bigwedge D\) is satisfiable iff \(T_{\varSigma (C)/E} \models \bigwedge E \, \wedge \, \bigwedge D\), where the variables C of \(E \cup D\) are seen as fresh new constants added to \(\varSigma \) to get a supersignature \(\varSigma (C) \supseteq \varSigma \), so that \(\bigwedge E \, \wedge \, \bigwedge D\) becomes a ground formula. This gives us, in modeltheoretic terms, the key to verify the soundness of the hopedfor reduction of the satisfiability for the theory of OS uninterpreted function symbols to that of the unsorted theory of uninterpreted function symbols: this reduction method will be sound if and only if the OS homomorphism \(h:T_{\varSigma (C)/E} \rightarrow T_{\varSigma (C)^{u}/E}_{u}\) is injective. In prooftheoretic terms this injectivity will hold if and only if for all ground \(\varSigma \)equation \(u=v\) we have the equivalence: \((\varSigma ,E) \vdash u=v \; \Leftrightarrow \; (\varSigma ^{u},E) \vdash u=v\). The \((\Rightarrow )\) direction is obvious, but the \((\Leftarrow )\) direction is a nontrivial new result that follows from several conservativity theorems that I prove in Sects. 3.2 and 4.1 by factoring the signature map \(u: \varSigma \rightarrow \varSigma ^{u}\) through a sequence \(\varSigma \hookrightarrow \varSigma ^{\Box } \rightarrow \widehat{\varSigma } \rightarrow \varSigma ^{u}\) of increasingly simpler ordersorted, manysorted and finally unsorted signatures and relating equational and rewriting deductions at all these levels.
The Plot Thickens. The soundness of the hopedfor reduction to the unsorted case for satisfiability modulo \(AC_{\varDelta }\) is a thornier issue. As before, the reduction will be sound if and only if for ground \(\varSigma \)equations E the unique \(\varSigma \)homomorphism \(h:T_{\varSigma /E \cup AC_{\varDelta }} \rightarrow T_{\varSigma ^{u}/E \cup AC_{\varDelta ^{u}}}_{u}\) from the initial \(E \cup AC_{\varDelta }\)algebra \(T_{\varSigma /E \cup AC_{\varDelta }}\) is injective. But some of the conservativity theorems along the above sequence of signature maps \(\varSigma \hookrightarrow \varSigma ^{\Box } \rightarrow \widehat{\varSigma } \rightarrow \varSigma ^{u}\) needed to make h injective actually break down in the \(AC_{\varDelta }\) case. The problem has to do with the translation of the equations \(AC_{\varDelta }\) along these signature maps. At the unsorted level of \(\varSigma ^{u}\) the translated equations \(AC_{\varDelta ^{u}}\), are more general and therefore identify more terms than the original OS equations \(AC_{\varDelta }\). Consider a simple example: the equation \(a+b=b+a\) does not type in our example signature \(\varSigma \), but it types in the supersignature \(\varSigma ^{\Box } \supseteq \varSigma \), which for our running example is depicted in Sect. 3.1. The AC equations \(AC_{\varDelta }\) in our example are just associativity and commutativity of \(+:A\;A \rightarrow A\) and therefore apply only to terms of sort A. Instead, the AC equations \(AC_{\varDelta ^{u}}\) are unsorted, and apply to all terms. This means that \(a+b =_{AC_{\varDelta ^{u}}} b+a\), but since b does not have sort A, we have \(a+b \not =_{AC_{\varDelta }} b+a\). It also means that the homomorphism \(h':T_{\varSigma ^{\Box }/E \cup AC_{\varDelta }} \rightarrow T_{\varSigma ^{u}/E \cup AC_{\varDelta ^{u}}}_{u}\) in general is not injective. However, all hope is not lost. As a direct consequence of Corollary 2 in Sect. 3.2, there is an isomorphism \(\alpha : T_{\varSigma /E \cup AC_{\varDelta }} \cong T_{\varSigma ^{\Box }/E \cup AC_{\varDelta }}_{\varSigma }\) to the \(\varSigma \)reduct of \(T_{\varSigma ^{\Box }/E \cup AC_{\varDelta }}\) and this shows that the homomorphism \(h:T_{\varSigma /E \cup AC_{\varDelta }} \rightarrow T_{\varSigma ^{u}/E \cup AC_{\varDelta ^{u}}}_{u}\) that we need to prove injective for the reduction to be sound is up to isomorphism a restriction of \(h'\) to \(T_{\varSigma /E \cup AC_{\varDelta }}\), which could be injective even if \(h'\) is not. Lemma 3 in Sect. 4.1 and the highly nontrivial Theorem 8 in Sect. 5 save the day: it follows from them that h is indeed injective and the reduction is also sound for the AC case. To the best of my knowledge the results on reducing ordersorted to unsorted satisfiability and on ordersorted rewriting and equality are new.
The paper is organized as follows. After some preliminaries in Sect. 2, the new results on orderrewriting and equality are given in Sect. 3. The reductions of satisfiability in the theory of OS uninterpreted function symbols (resp. OS uninterpreted function symbols modulo AC) to satisfiability in their respective unsorted theories is given in Sect. 4 (resp. Sect. 5). Related work and conclusions are discussed in Sect. 6. Due to space limitations no proofs are given; they can be found in the Technical Report [20].
2 Preliminaries on OrderSorted Algebra
The following material is adapted from [21], which generalizes [15]. It summarizes the basic notions of ordersorted algebra needed in the rest of the paper.
Definition 1
A manysorted signature is a pair \(\varSigma = (S, \varSigma )\), with S a set of sorts, and \(\varSigma \) and \(S^{*} \times S\)indexed set \(\varSigma =\{\varSigma _{w,s}\}_{{w,s}\in S^{*} \times S}\) of operation symbols, where \(S^{*}\) denotes the free monoid generated by S. We denote each \(f \in \varSigma _{w,s}\) as \(f: w \rightarrow s\). In particular, a constant of sort s is an operation \(a : \epsilon \rightarrow s\), with \(\epsilon \) the empty word.
An ordersorted (OS) signature is a triple \(\varSigma = (S, \le , \varSigma )\) with \((S,\le )\) a poset and \((S,\varSigma )\) a manysorted signature. \(\widehat{S} = S / \!\! \equiv _{\le }\), the quotient of S under the equivalence relation \(\equiv _{\le }\; = (\le \cup \ge )^{+}\), is called the set of connected components of \((S,\le )\). Note that a manysorted signature\(\varSigma \) is the special case where the poset \((S,\le )\) is discrete, i.e., \(s \le s'\) iff \(s=s'\).
The order \(\le \) and equivalence \(\equiv _{\le }\) are extended to sequences of same length in the usual way, e.g., \(s'_{1} \ldots s'_{n} \le s_{1} \ldots s_{n}\) iff \(s'_{i} \le s_{i}\), \(1 \le i \le n\). \(\varSigma \) is called sensible^{1} if for any two \(f: w \rightarrow s, f: w' \rightarrow s' \in \varSigma \), with w and \(w'\) of same length, we have \(w \equiv _{\le } w' \;\Rightarrow \; s \equiv _{\le } s'\).
Definition 2
For \(\varSigma = (S, \varSigma )\) a manysorted signature, a \(\varSigma \)algebra is an Sindexed set \(A=\{A_{s}\}_{s \in S}\) together with an assignment of: (i) to each constant \(a : \epsilon \rightarrow s\) of sort s an element \(A_{a}\in A_{s}\), and (ii) to each operation \(f: w \rightarrow s\), with \(w=s_{1}\ldots s_{n}\), \(n \ge 1\), a function \(A_{f: w \rightarrow s}: A^{w} \rightarrow A_{s}\), where, by convention, \(A^{s_{1}\ldots s_{n}}=A_{s_{1}} \times \ldots \times A_{s_{n}}\).

whenever \(s\le s'\), then we have \(A_{s} \subseteq A_{s'}\), and

whenever \(f: w\rightarrow s, f: w' \rightarrow s' \in f_{[s]}^{[s_{1}]\ldots [s_{n}]}\) and \(\overline{a} \in A^{w} \cap A^{w'}\), then we have \(A_{f:w\rightarrow s}(\overline{a}) = A_{f:w'\rightarrow s'}(\overline{a})\).
A manysorted\(\varSigma \)homomorphism\(h: A \rightarrow B\) is an Sindexed family of functions \(h=\{h_{s}:A_{s} \rightarrow B_{s}\}_{s \in S}\) such that: (i) for \(a: \epsilon \rightarrow s\), \(h_{s}(A_{a})=B_{a}\), and (ii) for \(f:w \rightarrow s\) with \(w \not =\epsilon \), \(A_{f};h_{s}=h^{w};B_{f}\).
An ordersorted\(\varSigma \)homomorphism\(h: A \rightarrow B\) is a manysorted \((S, \varSigma )\)homomorphism such that whenever \([s]=[s']\) and \(a \in A_{s} \cap A_{s'}\), then we have \(h_{s}(a) = h_{s'}(a)\). We call hinjective, resp. surjective, resp. bijective, iff for each \(s \in S\)\(h_{s}\) is injective, resp. surjective, resp. bijective. We call h an isomorphism if there is another ordersorted \(\varSigma \)homomorphism \(g: B \rightarrow A\) such that for each \(s \in S\), \(h_{s};g_{s}=1_{A_{s}}\), and \(g_{s};h_{s}=1_{B_{s}}\), with \(1_{A_{s}},1_{B_{s}}\) the identity functions on \(A_{s},B_{s}\). This defines a category \(\mathbf{OSAlg}_{\varSigma }\). \(\Box \)
Theorem 1

if \(a: \epsilon \rightarrow s\) then \(a \in T_{\varSigma ,s}\) (\(\epsilon \) denotes the empty string),

if \(t \in T_{\varSigma ,s}\) and \(s \le s'\) then \(t \in T_{\varSigma ,s'}\),

if \(f: s_{1}\ldots s_{n}\rightarrow s\) and \(t_{i}\in T_{\varSigma ,s_{i}} \; 1\le i \le n\), then \(f(t_{1},\ldots ,t_{n}) \in T_{\varSigma ,s}\),
For \([s] \in \widehat{S}\), \(T_{\varSigma ,[s]}\) denotes the set \(T_{\varSigma ,[s]}=\bigcup _{s' \in [s]}T_{\varSigma ,s'}\). Similarly, \(T_{\varSigma }\) will (ambiguously) denote both the abovedefined Ssorted set and the set \(T_{\varSigma }=\bigcup _{s \in S}T_{\varSigma ,s}\). We say that an OS signature \(\varSigma \)has nonempty sorts iff for each \(s \in S\), \(T_{\varSigma ,s} \not = \emptyset \). We will assume throughout that\(\varSigma \) has nonempty sorts.
An Ssorted set \(X=\{X_{s}\}_{s \in S}\) of variables, satisfies \(s \not = s' \Rightarrow X_{s}\cap X_{s'}=\emptyset \), and the variables in X are always assumed disjoint from all constants in \(\varSigma \). The \(\varSigma \)term algebra on variables X, \(T_{\varSigma }(X)\), is the initial algebra for the signature \(\varSigma (X)\) obtained by adding to \(\varSigma \) the variables Xas extra constants. Since a \(\varSigma (X)\)algebra is just a pair \((A,\alpha )\), with A a \(\varSigma \)algebra, and \(\alpha \) an interpretation of the constants in X, i.e., an Ssorted function \(\alpha \in [X {\small \rightarrow }A]\), the \(\varSigma (X)\)initiality of \(T_{\varSigma }(X)\) can be expressed as the following corollary of Theorem 1:
Theorem 2
(Freeness Theorem). If \(\varSigma \) is sensible, for each \(A \in \mathbf{OSAlg}_{\varSigma }\) and \(\alpha \in [X {\small \rightarrow }A]\), there exists a unique \(\varSigma \)homomorphim, \(\_\alpha : T_{\varSigma }(X) \longrightarrow A\) extending \(\alpha \), i.e., such that for each \(s \in S\) and \(x \in X_{s}\) we have \(x \alpha _{s} = \alpha _{s}(x)\).
The firstorder language of equational\(\varSigma \)formulas^{2} is defined in the usual way: its atoms are \(\varSigma \)equations\(t=t'\), where \(t,t' \in T_{\varSigma }(X)_{[s]}\) for some \([s] \in \widehat{S}\) and each \(X_{s}\) is assumed countably infinite. The set \( Form (\varSigma )\) of equational\(\varSigma \)formulas is then inductively built from atoms by: conjunction (\(\wedge \)), disjunction (\(\vee \)) negation (\(\lnot \)), and universal (\(\forall x\!\!:\!\!s\)) and existential (\(\exists x\!\!:\!\!s\)) quantification with sorted variables \(x\!\!:\!\!s \in X_{s}\) for some \(s \in S\). The literal \(\lnot (t=t')\) is denoted \(t \not = t'\).
Given a \(\varSigma \)algebra A, a formula \(\varphi \in Form (\varSigma )\), and an assignment \(\alpha \in [Y {\small \rightarrow }A]\), with \(Y= fvars (\varphi )\) the free variables of \(\varphi \), we define the satisfaction relation\(A,\alpha \models \varphi \) inductively as usual: for atoms, \(A,\alpha \models t = t'\) iff \(t \alpha = t' \alpha \); for Boolean connectives it is the corresponding Boolean combination of the satisfaction relations for subformulas; and for quantifiers: \(A,\alpha \models (\forall x\!\!:\!\!s)\; \varphi \) (resp. \(A,\alpha \models (\exists x\!\!:\!\!s)\; \varphi \)) holds iff for all \(a \in A_{s}\) (resp. some \(a \in A_{s}\)) we have \(A,\alpha \uplus \{(x \!\!:\!\! s,a)\} \models \varphi \), where the assignment \(\alpha \uplus \{(x\!\!:\!\!s,a)\}\) extends \(\alpha \) by mapping \(x\!\!:\!\!s\) to a. Finally, \(A \models \varphi \) holds iff \(A,\alpha \models \varphi \) holds for each \(\alpha \in [Y {\small \rightarrow }A]\), where \(Y= fvars (\varphi )\). We say that \(\varphi \) is valid (or true) in A iff \(A \models \varphi \). We say that \(\varphi \) is satisfiable in A iff \(\exists \alpha \in [Y {\small \rightarrow }A]\) such that \(A,\alpha \models \varphi \), where \(Y= fvars (\varphi )\).
An ordersorted equational theory is a pair \(T=(\varSigma ,E)\), with E a set of \(\varSigma \)equations. \(\mathbf{OSAlg}_{(\varSigma ,E)}\) denotes the full subcategory of \(\mathbf{OSAlg}_{\varSigma }\) with objects those \(A \in \mathbf{OSAlg}_{\varSigma }\) such that \(A \models E\), called the \((\varSigma ,E)\)algebras. \(\mathbf{OSAlg}_{(\varSigma ,E)}\) has an initial algebra\(T_{\varSigma /E}\) [21], further discussed in Sect. 3. Given \(T=(\varSigma ,E)\) and \(\varphi \in Form (\varSigma )\), we call \(\varphi \)Tvalid, written \(E \models \varphi \), iff \(A \models \varphi \) for each \(A \in \mathbf{OSAlg}_{(\varSigma ,E)}\). We call \(\varphi \)Tsatisfiable iff there exists \(A \in \mathbf{OSAlg}_{(\varSigma ,E)}\) with \(\varphi \) satisfiable in A. Note that \(\varphi \) is Tvalid iff \(\lnot \varphi \) is Tunsatisfiable.
\(\varSigma =((S,\le ),\varSigma )\) is a subsignature of \(\varSigma ' =((S',\le '),\varSigma ')\), denoted \(\varSigma \subseteq \varSigma '\), iff \((S,\le ) \subseteq (S',\le ')\) is a subposet inclusion, and \(\varSigma \subseteq \varSigma '\). A signature map\(H : \varSigma \rightarrow \varSigma '\) is a monotonic function \(H: (S, \le ) \rightarrow (S', \le ')\) of the underlying posets of sorts together with a mapping \(H: \varSigma \ni (f: s_{1} \ldots s_{n} \rightarrow s) \mapsto (H(f) : H(s_{1}) \ldots H(s_{n}) \rightarrow H(s)) \in \varSigma '\). H induces a map \(H: Form (\varSigma ) \rightarrow Form (\varSigma ')\). A signature inclusion \(\varSigma \subseteq \varSigma '\) defines a signature map \(\varSigma \hookrightarrow \varSigma ': f \mapsto f\).
3 OrderSorted Rewriting and Equality
Given an OS signature \(\varSigma =((S,\le ),\varSigma )\), a \(\varSigma \)rewrite rule^{3} is a sequent \(l \rightarrow r\) with \(l,r \in T_{\varSigma }(X)_{[s]}\) for some \([s]\in \widehat{S}\). An ordersorted term rewriting system (OSTRS) is then a pair \((\varSigma ,R)\) with R a set of \(\varSigma \)rewrite rules.
The above inference system yields as a special case a sound and complete inference system for ordersorted equational logic: we just view an ordersorted equational theory \((\varSigma ,E)\) as the OSTRS \((\varSigma ,R(E))\), where \(R(E)=\{t \rightarrow t' \mid t=t' \in E \;\; \vee \;\; t'=t \in E\}\). That is, equality steps are viewed as either lefttoright or righttoleft rewrite steps. We then have:
Definition 3
Theorem 3
The above theorem has as a corollary the construction of the initial algebra\(T_{\varSigma /E}\) for the category \(\mathbf{OSAlg}_{(\varSigma ,E)}\) of \((\varSigma ,E)\)algebras. Assuming \(\varSigma \) sensible, \(T_{\varSigma /E}\), has an easy definition. Note that the relation \(E \vdash u =v\) induces an equivalence relation \(=_{E}\) on each set \(T_{\varSigma ,[s]}\), \([s] \in \widehat{S}\). We then define \(T_{\varSigma /E,s'} =\{[t]_{=_{E}}\in T_{\varSigma ,[s]}/\!=_{E} \, \mid [t]_{=_{E}} \cap T_{\varSigma ,s'} \not = \emptyset \}\) for each \(s' \in [s]\), and define each operation \(f: s_{1} \ldots s_{n} \rightarrow s \in \varSigma \) by the map \(([t_1]_{=_{E}},\ldots ,[t_1]_{=_{E}}) \mapsto [f(t'_1,\ldots ,t'_n)]_{=_{E}}\), where \(t'_{i} \in [t_{i}]_{=_{E}} \cap T_{\varSigma ,s_{i}}\), \(1 \le i \le n\), showing it does not depend on the choice of \(t'_{i}\)’s.
3.1 KindComplete OSRewriting and Equational Deduction
The ordersorted rewrite relation \(t \rightarrow ^{\circledast } t'\) is obviously quite impractical and hard to implement. For this reason, given an OSTRS \((\varSigma ,R)\) several conditions on either \(\varSigma \) or R have been sought to be able to perform rewriting computations in essentially the standard and efficient way in which it is performed in an unsorted or manysorted TRS. Two such conditions, going back to [14], are to either: (i) require that the rules R are sortdecreasing, i.e., for each \(l \rightarrow r \in R\) and Ssorted substitution \(\sigma \), if \(l \sigma \in T_{\varSigma ,s}\) then \(r \sigma \in T_{\varSigma ,s}\) (this can be checked by the method explained in [17]); or (ii) if R is not sortdecreasing, extend \(\varSigma \) with new “retract operators” \(r_{s,s'}: s \rightarrow s'\), \(s,s' \in [s]\), \(s \not \le s'\), to catch typing errors, add to R “error recovery” rules of the form \(r_{s,s'}(x\!\!:\!\!s') \rightarrow x\!\!:\!\!s'\), and force sortdecreasingness of R by replacing each not sortdecreasing \(u \rightarrow v \in R\) by suitable rules of the form \(u\sigma \rightarrow r_{s,s'}(v\sigma )\), where \(\sigma \) may lower the sorts of some variables.
Conditions (i) or in its defect (ii) work and can be shown to be conservative in a certain sense [14]. However, they have serious limitations. Sort decreasingness is a strong condition that may be impossible to achieve for some OSTRS arising in practice; and if the solution with retracts is adopted, an unpleasant consequence is that we change the models, including the initial ones, since retracts add new operations and new error terms to the original sorts.
All these limitations can be avoided —while allowing rewriting with rules R and equational deduction with equations E to be performed in the standard way— by using a faithful embedding of ordersorted equational logic into membership equational logic (MEL) [3, 21]. MEL introduces a typing distinction between sorts\(s\in S\), which may be related by subsort relations just as in the ordersorted way, and the kind\(\top _{[s]}\) associated to each connected component \([s] \in \widehat{S}\), which is above all sorts in [s]. An illformed term like f(b) in the OS signature of the Introduction has no sort, but has kind \(\top _{[B]}\). In this way, the earlier side condition in the Congruence rule in Sect. 3 can be avoided.
The faithfulness of this embedding of logics means in particular that both initial models and equational deduction are preserved ([21], Corollary 28). However: (i) the proof in [21] is modeltheoretic; (ii) it focuses on the equational logic level, and does not deal with the more general rewriting logic level; and (iii) it assumes that the entire MEL framework is adopted. Can the essential advantages of this embedding be still obtained while remaining at the ordersorted level? The answer is yes! Since: (i) this solution plays a key role in the treatment of satisfiability for the theory of OS uninterpreted function symbols in Sect. 4, and (ii) having a much simpler theory of OS rewriting is useful in its own right, I give a detailed treatment of it below. The key idea is to use a signature transformation \(\varSigma \mapsto \varSigma ^{\Box }\) extending any OS signature \(\varSigma \) into one whose components have a top sort, understood as the kind of that component. The essential point is that \(\varSigma ^{\Box }\) belongs to a class of ordersorted signatures called kind complete where both rewriting and equational deduction can be performed in the standard way.
Definition 4
An OS signature \(\varSigma =((S,\le ),\varSigma )\) is called kindcomplete iff each connected component \([s] \in \widehat{S}\) has a top sort \(\top _{[s]}\), called its kind, with \(\top _{[s]} \ge s'\) for each \(s' \in [s]\), and any nonempty subsortpolymorphic family \(f_{[s]}^{[s_{1}]\ldots [s_{n}]} \subseteq \varSigma \) includes the typing \(f: \top _{[s_{1}]}, \ldots , \top _{[s_{n}]} \rightarrow \top _{[s]}\). Note that any manysorted \(\varSigma \) —and in particular any unsorted (i.e., singlesorted) \(\varSigma \)— is trivially kindcomplete.
Any OS signature \(\varSigma \) can be extended to a kindcomplete one by a transformation \(\varSigma \mapsto \varSigma ^{\Box }\). \(\varSigma ^{\Box }\) is constructed in twosteps: (i) we first associate to the ordersorted signature \(((S,\le ),\varSigma )\) the manysorted signature \(\widehat{\varSigma } = (\widehat{S}_{\top },\widehat{\varSigma })\), where \(\widehat{S}_{\top }=\{ \top _{[s]} \mid [s] \in \widehat{S}\}\), and with \(f: \top _{[s_{1}]} \ldots \top _{[s_{n}]} \rightarrow \top _{[s]}\in \widehat{\varSigma }\) iff \(f_{[s]}^{[s_{1}]\ldots [s_{n}]} \not = \emptyset \); and (ii) we then define \(\varSigma ^{\Box } = ((S \uplus \widehat{S}_{\top },\le _{\Box }), \varSigma \uplus \widehat{\varSigma })\), where \(\le _{\Box }\cap S^{2}=\; \le \), and for each \(\top _{[s]} \in \widehat{S}_{\top }\) we have \(s' <_{\Box } \top _{[s]}\) for each \(s' \in [s]\). That is, we add \(\top _{[s]}\) as a top sort above each \(s' \in [s]\) and add the new typing \(f: \top _{[s_{1}]} \ldots \top _{[s_{n}]} \rightarrow \top _{[s]}\) for each \(f_{[s]}^{[s_{1}]\ldots [s_{n}]} \not = \emptyset \).
For \(\varSigma \) the signature in the Introduction, \(\varSigma ^{\Box }\) is as follows:
Definition 5
Let \((\varSigma ,R)\) be an OSTRS with \(\varSigma \) sensible and kindcomplete. The onestepRrewrite relation \(u \rightarrow _{R} v\) holds between \(u,v\in T_{\varSigma }(X)_{[s]}\), \([s]\in \widehat{S}\), iff there is a rewrite rule \(t\rightarrow t' \in R\), a substitution \(\sigma \in [X {\small \rightarrow }T_{\varSigma }(X)]\), and a term position p in u such that \(u=u[t \sigma ]_{p}\) and \(v=u[t' \sigma ]_{p}\).
We denote by \(\rightarrow _{R}^{+}\) the transitive closure of \(\rightarrow _{R}\), and by \(\rightarrow _{R}^{*}\) the reflexivetransitive closure of \(\rightarrow _{R}\), and write \((\varSigma ,R) \vdash u \rightarrow _{R}^{*} v\) to make \(\varSigma \) explicit.
\((\varSigma ,R)\) is called terminating iff \(\rightarrow _{R}\) is a wellfounded relation; and is called confluent iff whenever \(t\rightarrow _{R}^{*}u\) and \(t\rightarrow _{R}^{*}v\) there exists w such that \(u\rightarrow _{R}^{*}w\) and \(v\rightarrow _{R}^{*} w\). \((\varSigma ,R)\) is called convergent iff it is both confluent and terminating. If \((\varSigma ,R)\) is convergent, each \(\varSigma \)term t rewrites by some \(t\rightarrow _{R}^{*}t!_{R}\) to a unique term \(t!_{R}\), called its Rcanonical form, that cannot be further rewritten.
When \(\varSigma \) is kindcomplete, if \(u\in T_{\varSigma }(X)_{[s]}\), \(t\rightarrow t' \in R\), and \(u=u[t \sigma ]_{p}\in T_{\varSigma }(X)_{[s]}\), then we always have \(u[t' \sigma ]_{p}\in T_{\varSigma }(X)_{[s]}\). That is, \(\rightarrow _{R}\)never produces illformed terms, so that in the above definition of \(\rightarrow _{R}\) the requirement the \(v\in T_{\varSigma }(X)_{[s]}\) is unnecessary and does not have to be checked. Indeed, for kindcomplete signatures ordersorted rewriting becomes standard sorted rewriting:
Lemma 1
Corollary 1
3.2 Conservativity Results
The whole point of the signature transformation \(\varSigma \mapsto \varSigma ^{\Box }\) is to replace complex deductions of the form \((\varSigma ,R) \vdash u \rightarrow ^{\circledast } v\) by simple rewrite sequences \( u \rightarrow _{R}^{*} v\) in the extended OSTRS \((\varSigma ^{\Box },R)\). But is this sound?
Theorem 4
Corollary 2
Since, besides the subsignature inclusion \(\varSigma \subseteq \varSigma ^{\Box }\), we also have the inclusion \(\widehat{\varSigma } \subseteq \varSigma ^{\Box }\), we have a further conservativity result:
Lemma 2
4 OrderSorted \((\varSigma ,\emptyset )\)QFSatisfiability
In theorem proving the theory \((\varSigma ,\emptyset )\), whose category of algebras is \(\mathbf{OSAlg}_{\varSigma }\), is called the theory of uninterpreted function symbols\(\varSigma \). As remarked in Definition 1, a manysorted signature \(\varSigma \) is a special case of an ordersorted signature, and an unsorted signature is a manysorted signature where \(S=\{U\}\) is a singleton set. Let \( QFForm (\varSigma ) \subseteq Form (\varSigma )\) denote the set of quantifierfree\(\varSigma \)formulas, i.e., formulas with no quantifiers. When \(\varSigma \) is unsorted, \((\varSigma ,\emptyset )\)QFsatisfiability, i.e., \((\varSigma ,\emptyset )\)satisfiability for any \(\varphi \in QFForm (\varSigma )\) is decidable [1]. The goal of this section is to show that the same holds for any sensible OS signature \(\varSigma \) by a reduction method. This can be done by two reductions. The first reduces this decidability problem to that of the OS word problem, which is the problem of whether, given a sensible OS signature \(\varSigma \) and a finite set \(E \cup \{u=v\}\) of ground\(\varSigma \)equations, \(E \vdash u=v\) holds or not. The desired first reduction is as follows:
Theorem 5
\((\varSigma ,\emptyset )\)QFsatisfiability is decidable for any sensible ordersorted signature \(\varSigma \) iff the OS word problem is decidable.
The proof follows from the more general Theorem 7 in Sect. 5, which deals with the OS word problem modulo equations B. The theorem’s algorithmic content mirrors its proof: \(\varphi = \bigvee _{1 \le i \le n}(\bigwedge E_{i} \, \wedge \, \bigwedge D_{i})\) in DNF with the \(E_{i}\) equalities and the \(D_{i}\) disequalities is satisfiable iff, when we view the variables in \(\varphi \) as fresh new constants C, there is an i, \(1 \le i \le n\), such that \(E_{i} \not \vdash u=v\) for each \(u \not = v \in D_{i}\). Furthermore, \(\bigwedge E_{i} \, \wedge \, \bigwedge D_{i}\) is satisfiable iff \(T_{\varSigma (C)/E_{i}} \models \bigwedge E_{i} \, \wedge \, \bigwedge D_{i}\).
The second reduction is from the OS word problem to the unsorted word problem. This is broken into two reductions: (i) of the manysorted word problem to the unsorted word problem in Sect. 4.1, and (ii) of the OS word problem to the manysorted word problem in Sect. 4.2.
For \(\varSigma \)unsorted and \(E \cup \{u=v\}\) a finite set of ground \(\varSigma \)equations it is wellknown that the word problem \(E \vdash u=v\) can be decided by a congruence closure algorithm [7, 24, 27]. What the various such algorithms have in common is that they are all instances (by applying difference strategies) of the same abstract congruence closure algorithm in the sense of [2], which is summarized below.
4.1 Abstract Congruence Closure
What the abstract congruence closure algorithm in [2] captures is what all concrete congruence closure algorithms have in common: they all are efficient, specialized ground KnuthBendix completion algorithms [2, 12, 16, 18]: they all begin with a set E of ground equations, and return a set R of convergent ground rewrite rules R equivalent to E (on a possibly extended signature). We can then decide the word problem \(E \vdash u=v\) by checking the syntactic equality \(u!_{R}=v!_{R}\).
The key notion of abstract congruence closure in [2] is then as follows:
Definition 6
[2] For \(\varSigma \) an unsorted signature and E a finite set of ground \(\varSigma \)equations, an abstract congruence closure for E is a set R of ground convergent \(\varSigma (K)\)rewrite rules, where K is a finite set of new constants, such that: (i) they are either of the form \(c \rightarrow c'\), with \(c,c' \in K\), or of the form \(f(c_{1},\ldots ,c_{n}) \rightarrow c\), with \(c_{1},\ldots ,c_{n},c \in K\), \(f \in \varSigma \) with \(n \ge 0\) arguments; (ii) for each \(c \in K\) there is a ground \(\varSigma \)term t such that \(t!_{R}=c!_{R}\); and (iii) for any ground \(\varSigma \)equation \(u=v\) we have \(E \vdash u=v\) iff we have the syntactic equality \(u!_{R}=v!_{R}\).
The paper [2] then gives an abstract congruence closure algorithm described by six inference rules, with an optional seventh, such that: (i) takes as input a triple \((\emptyset ,E,\emptyset )\) with E is a set of ground \(\varSigma \)equations; (ii) operates on triples of the form \((K',E',R')\) with \(E'\) (resp. \(R'\)) the current \(\varSigma (K')\)equations (resp. \(\varSigma (K')\)rules); and (iii) terminates with a triple of the form \((K,\emptyset ,R)\) such that R is a congruence closure for E. The name abstract congruence closure is welldeserved: the algorithms in [7, 24, 27], and two other ones, are all shown to be instantiations of the abstract algorithm by applying the inference rules with different strategies, so that both the operation of each algorithm and its actual complexity are faithfully captured by the corresponding instantiation [2].
We need to decide the manysorted word problem as a step for deciding the more general ordersorted one. But the manysorted word problem can be easily reduced to the unsorted one by means of the signature transformation \(\varSigma \ni (f: s_{1}\ldots s_{n} \rightarrow s) \mapsto (f: U \mathop {\ldots }\limits ^{n} U \rightarrow U) \in \varSigma ^{u}\), where \(\varSigma =(S,\varSigma )\) is a manysorted signature. Then all boils down to the following lemma:
Lemma 3
For \(\varSigma \) a sensible manysorted signature and E a set of regular\(\varSigma \)equations —i.e., t and \(t'\) have the same variables for each \(t=t'\in E\)— we have \((\varSigma ,E) \vdash u = v\) iff \((\varSigma ^{u},E^{u}) \vdash (u = v)^{u}\), where for any \(\varSigma \)equation \(t=t'\), \((t=t')^{u}\) leaves the terms unchanged but regards all variables as unsorted.
This lemma has a very practical consequence: we can use an unsorted congruence closure algorithm to solve the manysorted word problem at no extra cost: no changes are needed either to the input E or to the unsorted algorithm.
4.2 Deciding OS \((\varSigma ,\emptyset )\)QFSatisfiability
For any sensible OS signature \(\varSigma \) we have reduced the decidability of the \((\varSigma ,\emptyset )\)QFsatisfiability problem to that of the OS word problem in Theorem 5. And in Lemma 3 we have reduced the manysorted word problem to the unsorted word problem, which is decidable by a congruence closure algorithm. To prove the decidability of the OS \((\varSigma ,\emptyset )\)QFsatisfiability problem and obtain a correct algorithm for it we just need to reduce the OS word problem to the manysorted word problem. For this, the conservativity results in Sect. 3.2 are crucial:
Theorem 6
Therefore we can reuse the same algorithms and tools used in the unsorted case at no extra cost: the input to such algorithms and the algorithms or tools themselves need no changes, and the complexity is that of the unsorted case.
5 OrderSorted \((\varSigma , AC _{\varDelta })\)QFSatisfiability
Let \(\varSigma \) be a sensible OS signature with \(\varDelta \subseteq \varSigma \) made exclusively of binary function symbols, say, \(g,h,\ldots \), each of the form \(g: s\, s \rightarrow s\) for some sorts \(s\in S\), and with any typing of any such g in \(\varSigma \) necessarily a typing in \(\varDelta \), i.e., \(\varDelta \) and \((\varSigma \varDelta )\) share no symbols. Assume that each nonempty subsortpolymorphic family \(g_{[s]}^{[s]\,[s]} \subseteq \varDelta \) has always a biggest possible typing \(g: s_{g}\, s_{g} \rightarrow s_{g}\) such that for any other typing \(g: s\, s \rightarrow s\) in \(g_{[s]}^{[s]\,[s]}\) we have \(s \le s_{g}\). The equations: \(AC_{g}=\{g(x,y)=g(y,x), g(x,g(y,z))=g(g(x,y),z)\}\), with x, y, z of sort \(s_{g}\), express the associativitycommutativity (AC) of the subsortpolymorphic family \(g_{[s]}^{[s]\,[s]}\). We require that the axioms \(AC_{g}\) are sortpreserving, that is, that for each Ssorted substitution \(\sigma \) and each sort \(s \in S\) we have: \(g(x,y)\sigma \in T_{\varSigma }(X)_{s} \; \Leftrightarrow \; g(y,x)\sigma \in T_{\varSigma }(X)_{s}\), and \(g(x,g(y,z))\sigma \in T_{\varSigma }(X)_{s} \; \Leftrightarrow \; g(g(x,y),z)\sigma \in T_{\varSigma }(X)_{s}\), which can be easily checked by the method explained in [17]. Let \(AC_{\varDelta }\) denote the set \(AC_{\varDelta } =\bigcup _{g \in \varDelta }AC_{g}\) making all symbols in \(\varDelta \)AC. Call \((\varSigma , AC _{\varDelta })\) the OS theory of \(\varSigma \)uninterpreted function symbols\(\varSigma \)modulo\(AC_{\varDelta }\). When \(\varSigma =\varDelta \) is unsorted and has a single symbol \(+\), this is called the theory of commutative semigroups.
We can generalize the above setting by replacing \((\varDelta , AC _{\varDelta })\) by any OS theory \((\varDelta ,B)\) with \(\varDelta \) sensible and considering any sensible supersignature \(\varSigma \supseteq \varDelta \) with \(\varDelta \) and \(\varSigma  \varDelta \) not sharing any symbols. Call \((\varSigma ,B)\) the theory of uninterpreted function symbols\(\varSigma \)moduloB. We can then reduce the decidability of the \((\varSigma ,B)\)QFsatisfiabilty problem to that of the OS word problem modulo B, defined as the problem of whether given any \(\varSigma \supseteq \varDelta \) as above, and a set \(E \cup \{u=v\}\) of ground \(\varSigma \)equations, \(E \cup B \vdash u=v\) holds or not. The reduction is as follows:
Theorem 7
For any \((\varDelta ,B)\) and \(\varSigma \supseteq \varDelta \) as above, \((\varSigma ,B)\)QFsatisfiability is decidable iff the OS word problem modulo B is decidable.
For \(\varSigma \supseteq \varDelta \) unsorted, there are AC congruence closure algorithms for the theory \((\varSigma , AC _{\varDelta })\) [2, 19, 22] that decide the word problem modulo \( AC _{\varDelta }\) and therefore, by above Theorem 7, the unsorted \((\varSigma , AC _{\varDelta })\)QFsatisfiability problem. In the spirit of Sect. 4, the main goal of this section is to reduce the decidability of the OS \((\varSigma , AC _{\varDelta })\)QFsatisfiability problem to that of its unsorted version, and to furthermore reuse the same unsorted AC congruence closure algorithms in [2, 19, 22] to decide at no extra cost and with the same complexity the OS \((\varSigma , AC _{\varDelta })\)QFsatisfiability problem.
The decidability of OS \((\varSigma , AC _{\varDelta })\)QFsatisfiability has already been reduced to that of the OS word problem modulo \( AC _{\varDelta }\), now we just need to reduce the OS word problem modulo \( AC _{\varDelta }\) to the unsorted word problem modulo \( AC _{\varDelta ^{u}}\).
Theorem 8
6 Related Work and Conclusions
[11] presents the only ordersorted congruence closure algorithm I am aware of. It provides a good solution under some extra assumptions on \(\varSigma \), but it requires a quite complex congruence generation method and has worse complexity, \(O(n^{2})\), than the best \(O(n \; log (n))\) unsorted algorithms. The papers [2, 12, 16, 19, 22] present the view of congruence closure as completion. In particular, I have used abstract congruence closure [2] and ACcongruence closure [2, 19, 22]. The modular combination of congruence closure, AC congruence, and polynomial ring congruence closure algorithms for different symbols and its relation to the NelsonOppen combination method [23, 25] is studied in [31]. Likewise, the combination of AC congruence closure with other satisfiability algorithms using the Shostak combination method [28] is studied in [5] The first general study I know of satisfiability modulo theories in an ordersorted setting is [30].
The abovementioned work has influenced and motivated the present one. The good news is that we get all the benefits of ordersorted \((\varSigma ,\emptyset )\) and \((\varSigma ,AC_{\varDelta })\)satisfiability for free, with no added computational cost and being able to reuse unsorted tools. At a more theoretical level, the ordersorted rewriting and equality results presented here are also good news and belong to the foundations of such an area. Future work will focus on exploiting these results at the tool level.
Footnotes
 1.
The notion of a sensible signature is a minimal syntactic requirement to avoid excessive ambiguity. For example, a manysorted signature \(\varSigma \) with sorts A, B and C, constant \(a: \epsilon \rightarrow A\) and operations \(f:A \rightarrow B\) and \(f:A \rightarrow C\) is not sensible and therefore is intrinsically ambiguous: the term f(a) has both sorts B and C, which are completely different sorts.
 2.
There is only an apparent lack of predicate symbols. To express a predicate \(p(x_{1}\!\!:\!\!s_{1},\ldots ,x_{n}\!\!:\!\!s_{n})\), add a new sort \( Truth \) with a constant \( tt \), and with \(\{ Truth \}\) a separate connected component, and view p as a function symbol \(p:s_{1},\ldots ,s_{n}\rightarrow Truth \). An atomic formula \(p(t_{1},\ldots ,t_{n})\) is then expressed as the equation \(p(t_{1},\ldots ,t_{n})= tt \).
 3.
For greater generality no restriction is placed on the variables of l and r.
Notes
Acknowledgements
Partially supported by NSF Grant CNS 1319109. I thank Maria Paola Bonacina for suggested improvements.
References
 1.Ackermann, W.: Solvable Cases of the Decision Problem. NorthHolland Publishing Company, Amsterdam (1954)zbMATHGoogle Scholar
 2.Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. Autom. Reasoning 31(2), 129–168 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
 3.Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. Theoret. Comput. Sci. 236, 35–132 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
 4.Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., MartíOliet, N., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
 5.Conchon, S., Contejean, E., Iguernelala, M.: Canonized rewriting and ground AC completion modulo Shostak theories : design and implementation. Logical Methods Comput. Sci. 8(3), 1–29 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
 6.Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. NorthHolland Publishing Company, Amsterdam (1990)Google Scholar
 7.Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. J. ACM 27(4), 758–771 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
 8.Frisch, A.M.: The substitutional framework for sorted deduction: fundamental results on hybrid reasoning. Artif. Intell. 49(1–3), 161–198 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
 9.Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, Singapore (1998)zbMATHGoogle Scholar
 10.Futatsugi, K., Goguen, J., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. In: Proceedings of POPL 1985, pp. 52–66. ACM (1985)Google Scholar
 11.Gallier, J., Isakowitz, T.: Ordersorted congruence closure. Technical report CIS686, UPenn (1988). http://repository.upenn.edu/cis_reports/686
 12.Gallier, J.H., Narendran, P., Plaisted, D.A., Raatz, S., Snyder, W.: An algorithm for finding canonical sets of ground rewrite rules in polynomial time. J. ACM 40(1), 1–16 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
 13.Gnaedig, I., Kirchner, C., Kirchner, H.: Equational completion in ordersorted algebras. Theoret. Comput. Sci. 72(2–3), 169–202 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
 14.Goguen, J., Jouannaud, J.P., Meseguer, J.: Operational semantics of ordersorted algebra. In: Brauer, W. (ed.) Automata, Languages and Programming. LNCS, vol. 194, pp. 221–231. Springer, Heidelberg (1985)CrossRefGoogle Scholar
 15.Goguen, J., Meseguer, J.: Ordersorted algebra I. Theoret. Comput. Sci. 105, 217–273 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
 16.Kapur, D.: Shostak’s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 23–37. Springer, Heidelberg (1997)CrossRefGoogle Scholar
 17.Kirchner, C., Kirchner, H., Meseguer, J.: Operational semantics of OBJ3. In: Lepistö, T., Salomaa, A. (eds.) Automata, Languages and Programming. LNCS, vol. 317, pp. 287–301. Springer, Heidelberg (1988)CrossRefGoogle Scholar
 18.Knuth, D., Bendix, P.: Simple word problems in universal algebra. In: Leech, J. (ed.) Computational Problems in Abstract Algebra. Pergamon Press, Oxford (1970)Google Scholar
 19.Marché, C.: On ground ACcompletion. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 411–422. Springer, Heidelberg (1991)CrossRefGoogle Scholar
 20.Meseguer, J.: Ordersorted rewriting and congruence closure. Technical report, C.S. Department, University of Illinois at UrbanaChampaign, June 2015. http://hdl.handle.net/2142/78008
 21.Meseguer, J.: Membership algebra as a logical framework for equational specification. In: ParisiPresicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)CrossRefGoogle Scholar
 22.Narendran, P., Rusinowitch, M.: Any ground associativecommutative theory has a finite canonical system. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 423–434. Springer, Heidelberg (1991)CrossRefGoogle Scholar
 23.Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)CrossRefzbMATHGoogle Scholar
 24.Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
 25.Oppen, D.C.: Complexity, convexity and combinations of theories. Theoret. Comput. Sci. 12, 291–302 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
 26.SchmidtSchauss, M.: Computational Aspects of OrderSorted Logic with Term Declarations. LNCS (LNAI), vol. 395. Springer, Heidelberg (1989)CrossRefzbMATHGoogle Scholar
 27.Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7), 583–585 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
 28.Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1–12 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
 29.Smolka, G., AïtKaci, H.: Inheritance hierarchies: semantics and unification. J. Symb. Comput. 7(3/4), 343–370 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
 30.Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 641–653. Springer, Heidelberg (2004)CrossRefGoogle Scholar
 31.Tiwari, A.: Combining equational reasoning. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 68–83. Springer, Heidelberg (2009)CrossRefGoogle Scholar
 32.Walther, C.: A mechanical solution of Schubert’s steamroller by manysorted resolution. Artif. Intell. 26(2), 217–224 (1985)MathSciNetCrossRefzbMATHGoogle Scholar