Revista Colombiana de Matemáticas Volumen 31 (1997), páginas 77–98

A deductive calculus for conditional equational systems with built-in predicates as premises

Mauricio Ayala-Rincón Universidade de Brasília, BRASIL

Abstract. Conditional equationally defined classes of many-sorted algebras, whose premises are conjunctions of (positive) equations and builtin predicates (constraints) in a basic first-order theory, are introduced. These classes are important in the field of algebraic specification because the combination of equational and built-in premises give rise to a type of clauses which is more expressive than purely conditional equations. A sound and complete deductive system is presented and algebraic aspects of these classes are investigated. In particular, the existence of free algebras is examined. Key words and phrases. Algebraic specification, rewriting systems, theorem proving. 1991 AMS Mathematics Subject Classification. Primary 68Q65. Secondary 68Q42, 68T15, 03C05, 08A70.

1. Introduction

The need to use conditional equations appears initially in universal algebra in order to represent some algebraic structures, for example the left cancellative law can be expressed by the conditional equation x ∗ y = x ∗ z ⟹ y = z. Classes of algebras presented by equations and conditional equations are called varieties and quasivarieties (or positive equational universal Horn classes), respectively. The use of conditional equations has also been studied in the fields of abstract data types and algebraic specification because they provide easier and more elegant specifications having a greater expressive power than (unconditional) equations.

A combination of many-sorted (positive equational) universal Horn clauses with built-in predicates in a basic theory as premises is considered. The purpose of this combination is to improve the expressiveness of the (positive equational) universal Horn clauses in such a way that one can request for (not necessarily equational) predicates in a first-order theory over a specific signature. Built-in predicates are logical objects that are incorporated (as conditions) into the syntactical structure of (positive equational) universal Horn clauses. This gives rise to a class of conditional clauses with conditions formed by a built-in predicate and the usual conjunction of equations, of the following form:

u_{1} = v_{1} ∧ ⋯ ∧ u_{n} = v_{n} ∧ C ⟹ u = v.

Universal Horn classes with built-in predicates are presented by this type of clauses. These combined classes are more expressive than quasivarieties since theories which cannot be axiomatized by universal Horn clauses can be incorporated as built-in predicates.

It is well-known that free algebras exist for varieties as well as for quasivarieties. In contrast, this is not a natural property of universal Horn classes with built-in predicates because, for instance, the built-in predicates can be negative equational conditions and in general negative conditional equationally defined classes have no free algebras. However, under certain restrictions which can be conceived as a type of initiality property (or restriction to the standard model) of the basic theory, the existence of free and even initial algebras is guaranteed.

Conditional rewriting has been suggested as the basic operational mechanism for deduction in universal Horn classes with built-in predicates [AR93]. Conditional rewriting systems have been used for equational deduction in conditional equationally defined classes of algebras. Sets of equations and conditional equations can be considered as functional programs with rewriting as its computation mechanism. Whereas predefined operations are available in common programming languages they are not naturally incorporated into rewriting techniques. Therefore it is of great interest to amalgamate built-in algorithms and rewriting.

This work is focused on the algebraic (not on the operational) properties of positive equational universal Horn classes with built-in predicates. Firstly, basic theories are defined. Afterwards, the syntax and semantics of specifications with combined premises (conjunctions of equations and predicates in a basic theory) are investigated. Finally, a deductive calculus for this class of specifications is introduced, its completeness proved and appropriate restrictions to guarantee the existence of free algebras are given.

Related work: Already O’Donnell considered arbitrary predicates as conditions of rules [O’D77]. Padawitz [Pad88] has presented in detail a calculus for universal Horn clauses from the algebraic point of view. His approach is more general than that presented here, because he does not separate between logic and algebraic concepts. Here this separation is necessary because in the present work the intention is to formalize an operational approach: the combination of decision procedures for evaluating many-sorted first-order logic predicates and deduction based on term rewriting techniques for manipulating the whole specification. With more detail than Padawitz (at least from the operational point of view), Kaplan [Kap83], [Kap84] has developed a calculus for equational universal Horn clauses but without the special kind of built-in predicates incorporated here. Kaplan’s work is important principally because he was the first person developing with precision an operational approach to manipulate these restricted classes of universal Horn clauses by extending the well-known purely equational rewriting techniques. Vorobyov [Vor89] has treated deduction for conditional specifications whose conditions are built-in predicates combining rewriting and built-in algorithms. Kirchner, Kirchner and Rusinowitch [KKR90] have focused the deduction from the point of view of constraints. Neither Vorobyov nor the other authors admit standard equational conditions as it is done in this work. Efforts to combine built-in predicates (and their corresponding decision procedures) and equational conditions as premises of conditional specifications, were made in [AR93].

Dershowitz and Okada [DO90] studied conditional rewriting systems with (informal) built-in predicates and standard equational conditions as premises. They briefly treated termination, confluence and a critical pair criterion for their systems. Precise proofs of their suggested results on confluence can be found in [AR94]. Avenhaus and Becker [AB92] presented a method to integrate built-in operations that are described by a given built-in algebra into conditional rewriting. They do not allow new sorts in the extended signature and the variables are restricted to range over basic terms. Later on Becker [Bec94] presented an operationalization of clausal specifications where the axioms are positive/negative conditional equations admitting predefined algebras. The clauses are treated by rewriting. His approach can be considered as an attempt to provide a general framework to handle specifications with predefined algebras in a semantically clean way.

The principal differences between the present approach (and Vorobyov’s approach) and the previous ones is that whereas here all models of the basic theory are considered, they work with a specific model of the basic theory giving restrictions and assumptions on the built-in part which allow an operational treatment by purely rewriting and validity check avoiding case-splittings. Their approaches are appropriate to compute in algebraic structures with built-in parts but they are not sufficient for equational deduction (neither in the whole theory nor in the initial theory).

An extended abstract of this work appears in [AR95].

2. Basic theories

Appropriate definitions of basic theories, whose objects will be further incorporated (as conditions) into the syntactical structure of universal Horn clauses, are given. Basic knowledge about algebraic specification (see [EM85],[Wec92]) and model theory is assumed (see [CK90], [Gal87]).

By adding to the formalism of first-order logic (with equality) the notion of sort, one obtains a flexible logic called many-sorted first-order logic (with equality) (see [Gal87]), which enjoys the same properties as first-order logic. The purpose of many-sorted first-order theories is to express properties of structures of different sorts which appear when one is interested in axiomatizing data structures found in computer science (lists of natural numbers, arrays of objects indexed by integers, etc.).

Definition 2.1. An S_{0}-sorted signature is a set Σ_{0}, whose elements are called operation (or function) and predicate symbols, together with an arity function AR : Σ_{0} → S_{0}^{∗} × (S_{0} ∪ {λ}), which assigns to each operation symbol f of Σ_{0} an ordered pair (w, s) and to each predicate symbol p of Σ_{0} an ordered pair (w, λ) with their first component w a word over S_{0}, called the arity or domain of f or p, respectively, and their second component s an element of S_{0}, called the sort or range of f, and λ meaning that p is a predicate symbol, respectively.

The language of many-sorted first-order logic is given by an S_{0}-sorted signature Σ_{0}; a family of disjunct countably infinite sets V_{s} of variables for every sort s ∈ S_{0} (V_{0} = ⋃_{s∈S_{0}} V_{s}); the logical connectives &, ¬ and the logical universal quantifier ∀^{1}; one binary relation symbol =^{2} and auxiliary symbols (,).

The notions of (well-formed) term and formula, atomic formula, free and bound occurrences of a variable in a formula, universal and existential closure of a formula sentences (i.e., formulae with no free variables) and of quantifierfree formulae (i.e., formulae with no bound variables) are assumed to be known. t(x_{1}, …, x_{n}) denotes a term t whose variables belong to {x_{1}, …, x_{n}}. Similarly, P (x_{1}, …, x_{n}) denotes a formula whose free variables form a subset of {x_{1}, …, x_{n}}.

1The others logical connectives (i.e., ∨, ⇒, ⇔) and the existential quantifier (∃) can be seen as abbreviations of &, ¬ and ∀. For example, ∃xP (x) is an abbreviation of ¬∀x¬P (x).

2To be more precise, one should consider one binary relation symbol =_{s} and one universal quantifier ∀_{s} for each sort s ∈ S.

As usual, logical axioms and rules of inference (modus ponens and universal generalization) are needed to transform the above syntactical notions into a formal system.

For a set of sentences T and a formula P, ⊢ P and T ⊢ P mean that P is a theorem of Σ_{0} and that there is a proof of P from the logical axioms and T, respectively. As the logical axioms are always assumed, it is said that there is a proof of P from T, or P is deducible from T, whenever T ⊢ P.

Definition 2.2. A set T of sentences of Σ_{0} is said to be inconsistent iff every formula of Σ_{0} can be deduced from T. Otherwise T is consistent. A sentence P is consistent iff {P } is. A sentence P is said to be T -consistent iff T ∪ {P } is. A quantifier-free formula P (x_{1}, …, x_{n}) is said to be T -consistent iff its existential closure ∃x_{1}, …, x_{n}(P (x_{1}, …, x_{n})) is T -consistent.

Definition 2.3. An interpretation 𝔄 for Σ_{0} consists of an S_{0}-sorted universe A_{0} = ⋃_{s∈S_{0}}A_{s}, where A_{s} ≠ ∅ for all s ∈ S_{0}. In this universe, each predicate symbol p : w and each operation symbol f : w → s in Σ_{0} correspond to a w-placed relation p^{𝔄} : A^{w} and to a function f^{𝔄} : A^{w} → A_{s}, respectively. Nullary operation symbols f : → s correspond to constants.

As usual the notation 𝔄 ⊧ P is used to denote that the sentence P is valid in the interpretation 𝔄 or, equivalently, that 𝔄 is a model of P.

Definition 2.4. Given a set of sentences T. 𝔄 is said to be a model of T iff 𝔄 is a model of each P in T. As usual, this is denoted by 𝔄 ⊧ T. A sentence or a set of sentences is satisfiable iff it has at least one model. A sentence is a logical consequence of a set of sentences T, in symbols T ⊧ P, iff every model of T is a model of P. A set of axioms of a theory T_{0} is a set of sentences with the same logical consequences as T_{0}.

Remark 2.5. Although many-sorted first-order logic is very convenient, it is not an essential extension of standard one-sorted first-order logic in the sense that there is a translation of many-sorted logic into one-sorted logic. For details see [Gal87]. In this work, results of the classical one-sorted first-order logic are indiscriminately applied to the many-sorted first-order logic. ◁

A basic theory is defined as follows.

Definition 2.6. A basic theory T_{0} of Σ_{0} is an arbitrary (consistent) manysorted first-order theory with equality.

The Presburger arithmetic (PAR), the additive number theory (AN T ) and the successor arithmetic (SA) are examples of (one-sorted) basic theories. The language of the successor arithmetic consists of the constant 0, the unary function symbol s for successor and binary relation ≤. SA is the set of all first-order formulae from this language valid in the standard model of natural numbers, where all symbols get their usual meanings. The Presburger arithmetic (or theory of integers under addition) was originally defined over the domain of integers with the usual constants 0 and 1 and with arithmetical equality and addition only. It is well-known that the Presburger arithmetic is not finitely axiomatizable but it was showed that it is decidable and complete, by the method of elimination of quantifiers [Pre29] (see for example [Coo72] for a relatively efficient algorithm using this method). Presburger’s proof was extended later to include all the usual arithmetical relations (<, >, ≤, ≥, =) over the domain of integers.

In this work Presburger formulae will be considered as those that can be built up from integer constants, integer variables, addition, the usual arithmetical relation “<”, the first-order logical connectives and quantification. Formulae take their usual meaning. For example, the formula ∀x∃y(2y + x < 3 ⇒ x < y) falls within this class. Note that nx is an abbreviation for repeated addition but arbitrary multiplication is not permitted. The other arithmetical relations may easily be added; for example, x = y can be defined as x < y+1 & y < x+1 and x ≥ y as y < x + 1.

A unquantified Presburger formulae is a Presburger formulae having no quantifiers. The unquantified Presburger arithmetic, consisting of those unquantified Presburger formulae in the Presburger arithmetic, is decidable as subclass of the Presburger arithmetic. In particular, this subclass of formulae may be decided by Bledsoe’s SUP-INF method; see [Sho81, ARG97].

3. Universal Horn clauses with built-in predicates

Built-in predicates are logical objects that are incorporated (as conditions) into the syntactical structure of universal Horn clauses. This results in a class of conditional clauses with conditions formed by the usual conjunction of equations and a built-in predicate.

Definition 3.1. Built-in predicates are quantifier-free formulae of a basic theory.

Remark 3.2. The unquantified SA, PAR and AN T are decidable as subclasses of decidable theories. To consider only quantifier-free formulae appears to be very restrictive, however this is not the case because many existential quantified formulae can be abbreviated to new built-in predicate symbols; for instance, the formula ∃x(x + x = y), in the Presburger arithmetic, can be conceived as the predicate Even(y).

This restriction is made to incorporate the built-in predicates as conditions into the universal Horn clauses with one general universal quantifier for the whole clause. ◁

In order to incorporate the built-in predicates as conditions into the structure of universal Horn clauses (defined in an S-sorted signature Σ), built-in objects are described in a built-in language given by an S_{0}-sorted signature Σ_{0}, as mentioned above, with the following restrictions:

Restriction 3.3 (on the signatures). Let Σ_{0} be an S_{0}-sorted signature, the built-in language of a basic theory T_{0}. The introduction of new “syntactical” function symbols is captured as usual by the notion of a signature extension. Let S_{0} and S be two sets of sorts such that S_{0} ⊆ S. Let Σ_{0} and Σ be S_{0}- and S-sorted signatures, respectively. Suppose that Σ ∖ Σ_{0} does not contain function symbols with sort in S_{0}. Terms with sort in S_{0} are called basic terms and in S ∖ S_{0} extended terms.

The previous restriction separates built-in from extended terms in such a way that the conservativeness of the extension is guaranteed.

The following example illustrates a signature with the Presburger arithmetic as built-in theory.

Example 3.4. Let S_{0} = {int}, S = S_{0} ∪ {array, element} be sets of sorts and Σ_{0} and Σ be S_{0}- and S-sorted signatures, respectively, with the following declarations:

Σ_{0} : …, −1, 0, 1, …: → int

+  : int × int → int
<  : int × int

Σ : ⟨ , , ⟩  : array × int × element → array

[ ]  : array × int → element

Note that the predicates of the basic signature Σ_{0} have no range. However they have a logical interpretation that will be syntactically embedded into the extended specification. Constants …, −1, 0, 1, … are given because it will be assumed that the built-in language is sufficiently expressive to give a ground term for any element of the models of interest. This can be made without mentioning explicitly all integer constants. ◁

Definition 3.5. Let S_{0}, S, Σ_{0}, Σ and T_{0} be restricted as before. (Σ, Σ_{0}, T_{0}) is said to be a signature with built-in theory T_{0} over Σ_{0}.

Definition 3.6. Let (Σ, Σ_{0}, T_{0}) be a signature with built-in theory T_{0} over Σ_{0}. A Σ-algebra over the built-in theory T_{0}, � consists of a model 𝔄 of T_{0} with universe A_{0}, an S-sorted set A, whose restriction to S_{0} is precisely A_{0}, and of a family of operations such that every operation symbol f : w → s of Σ∖Σ_{0} is realized as an operation f� : A^{w} → A_{s}, every operation symbol f : w → s of Σ_{0} as f^{𝔄} and every predicate symbol p : w of Σ_{0} as p^{𝔄}. When Σ is unspecified or unemphasized, a Σ-algebra over T_{0} is simply said to be an algebra over T_{0}.

Observe that this notion of Σ-algebra embodies an interpretation of the basic signature and even a model of T_{0}. This is a slight generalization of the usual notion of algebra which is well suited for the actual purposes.

In the sequel, when a Σ-algebra � is mentioned it will be assumed that A, 𝔄 and A_{0} are its carrier set, its basic model and basic universe, respectively. The same for �, B, 𝔅 and B_{0}.

Definitions of algebraic notions for Σ-algebras over built-in theories (viz subalgebra, homomorphism, direct product, direct limit, etc.) are not evident. In particular, note that one cannot straightforwardly adapt the definition of direct product for Σ-algebras over built-in theories because the interpretation of predicates is not obvious. For example, let 𝔄 be a model of SA and consider the direct product A_{0} × A_{0} of its carrier set. The predicate ≤ cannot be interpreted for pairs in this direct product of sets; for instance, an interpretation for (0, s(0)) ≤ (s(0), 0) is not evident. The notion of subalgebra can be adapted for Σ-algebras over built-in theories by restricting the basic mod el of the algebra to remain identical in every subalgebra. The notion of homomorphism can also be defined by appropriately combining the logical and the algebraic notions as follows.

Definition 3.7. Let 𝔄, 𝔅 be models of a basic theory, T_{0} over Σ_{0}, with universes A and B respectively. 𝔅 is said to be homomorphic to 𝔄 if and only if there is an S_{0}-sorted surjective mapping h : A → B satisfying the following conditions:

• For each predicate symbol p : w in Σ_{0} and respective relations p^{𝔄} ⊆ A^{w} and p^{𝔅} ⊆ B^{w} and all n-tuples (x_{1}, …, x_{n}) ∈ A^{w}, if p^{𝔄}(x_{1}, …, x_{n}) then p^{𝔅}(h(x_{1}), …, h(x_{n})).

• For each operation symbol f : w → s in Σ_{0} and respective functions f^{𝔄} : A^{w} → A_{s} and f^{𝔅} : B^{w} → B_{s} and for all n-tuples (x_{1}, …, x_{n}) ∈ A^{w}, h(f^{𝔄}(x_{1}, …, x_{n})) = f^{𝔅}(h(x_{1}), …, h(x_{n})).

A mapping h satisfying the above is called a homomorphism of 𝔄 onto 𝔅. An isomorphism between 𝔄 and 𝔅 is a bijective homomorphism of 𝔄 onto 𝔅, such that for each predicate symbol p : w in Σ_{0} and respective relations p^{𝔄} ⊆ A^{w} and p^{𝔅} ⊆ B^{w} and all n-tuples (x_{1}, …, x_{n}) ∈ A^{w}, p^{𝔄}(x_{1}, …, x_{n}) iff p^{𝔅}(h(x_{1}), …, h(x_{n})).

Observe that in the above definition, 𝔄 and 𝔅 are both assumed to be models of a basic theory T_{0}. Without this assumption, the existence of a homomorphism of a model 𝔄 of a theory T_{0} onto 𝔅 does not imply that 𝔅 is a model of T_{0}. This is proved, for instance, by the fact that quasivarieties are not closed under homomorphic images. On the other hand, if 𝔄 is a model of a first-order theory T_{0} and there is an isomorphism between 𝔄 and 𝔅 then 𝔅 is also a model of T_{0}. This follows from the notion of elementary equivalence and Lyndon homomorphism theorem; see [CK90].

Definition 3.8. Let (Σ, Σ_{0}, T_{0}) be a signature and let � and � be Σ-algebras. An S-sorted mapping h : A → B, whose restriction to A_{0} is a homomorphism of 𝔄 onto 𝔅, is called a Σ-homomorphism if h(f� (x_{1}, …, x_{n})) = f� (h(x_{1}), …, h(x_{n})) for all operation symbols f : w → s in Σ ∖ Σ_{0} and all n-tuples (x_{1}, …, x_{n}) ∈ A^{w}.

An S-sorted set of variables V = ⋃_{s∈S} V_{s} is fixed. Each V_{s} is a countably infinite set of variables of sort s. As before, V_{0} denotes the set ⋃_{s∈S_{0}} V_{s} of basic variables.

Definition 3.9. The S-sorted set of all Σ-terms over V, denoted by T_{Σ}(V) is defined as follows: T_{Σ}(V) = (T_{Σ}(V)_{s}|s ∈ S), where each set T_{Σ}(V)_{s} of Σ-terms over V of sort s is recursively defined as the least set of words over Σ ∪ V_{s} such that V_{s} ⊆ T_{Σ}(V)_{s} and, for all operation symbol f : w → s in Σ and all tuples (t_{1}, …, t_{n}) ∈ (T_{Σ}(V))^{w}, f(t_{1}, …, t_{n}) belongs to T_{Σ}(V)_{s}.

Note that for all predicate symbols p : w in Σ_{0}, and all tuples (t_{1}, …, t_{n}) ∈ (T_{Σ}(V))^{w}, p(t_{1}, …, t_{n}) expresses the predicate symbol applied to such a tuple (but it does not belong to T_{Σ}(V)). Moreover, observe that with all predicate symbols p in Σ_{0}, the logical connectives, universal quantifier, equality, etc. and the terms in T_{Σ}(V) (or, more precisely, in T_{Σ_{0}}(V_{0})), all possible basic formulae can be constructed.

An interpretation in T_{Σ}(V) of all terms (in T_{Σ}(V)) and all possible predicate expressions (formed from predicate symbols p : w in Σ_{0} and tuples (t_{1}, …, t_{n}) in (T_{Σ}(V))^{w}) is given as follows.

Definition 3.10. All terms t in T_{Σ}(V) and predicate expressions formed from a predicate symbol p : w ∈ Σ_{0} and a tuple (t_{1}, …, t_{n}) ∈ (T_{Σ}(V))^{w} have the following interpretation:

• if t ≡ x ∈ V then x^{T_{Σ}(V)} = x;

• if t ≡ f(t_{1}, …, t_{n}) for some function symbol f : w → s in Σ and (t_{1}, …, t_{n}) ∈ (T_{Σ}(V))^{w} then f^{T_{Σ}(V)}(t_{1}, …, t_{n}) = f(t_{1}, …, t_{n});

• p^{T_{Σ}(V)}(t_{1}, …, t_{n}) (or simply, p(t_{1}, …, t_{n})) iff T_{0} ⊧ p(t_{1}, …, t_{n}).

In the sequel, when T_{Σ}(V) is mentioned, it is supposed that all terms and predicate expressions are interpreted as above. It can be seen that T_{Σ}(V) restricted to basic terms is an interpretation for the built-in language Σ_{0}. T_{Σ}(V) is called the term Σ-interpretation for Σ_{0}.

Definition 3.11. A congruence on T_{Σ}(V) is an S-sorted equivalence relation R compatible with operation and predicate symbols: for all operation symbols f : w → s in Σ, if (a_{1}, …, a_{n}), (b_{1}, …, b_{n}) ∈ (T_{Σ}(V))^{w} and (a_{i}, b_{i}) ∈ R, for all i = 1, …, n, then R includes (f^{T_{Σ}(V)}(a_{1}, …, a_{n}), f^{T_{Σ}(V)}(b_{1}, …, b_{n})) and for all predicate symbols p : w in Σ_{0}, if (a_{1}, …, a_{n}), (b_{1}, …, b_{n}) ∈ (T_{Σ}(V))^{w}, (a_{i}, b_{i}) ∈ R, for all i = 1, …, n, and p^{T_{Σ}(V)}(a_{1}, …, a_{n}) then p^{T_{Σ}(V)}(b_{1}, …, b_{n}).

The quotient T_{Σ}(V)/R is defined as follows:

• the carrier of T_{Σ}(V)/R is the set of equivalence classes

{[a] = {b|(b, a) ∈ R} | a ∈ T_{Σ}(V)},

denoted also by T_{Σ}(V)/R;

• ∀P : w ∈ Σ_{0}, ∀(a_{1}, …, a_{n}) ∈ (T_{Σ}(V))^{w}, P^{T_{Σ}(V)/R}([a_{1}], …, [a_{n}]) whenever P^{T_{Σ}(V)}(a_{1}, …, a_{n});

• ∀f:w →s ∈ Σ, ∀(a_{1}, …, a_{n}) ∈ (T_{Σ}(V))^{w}, f^{T_{Σ}(V)/R}([a_{1}], …, [a_{n}]) = [f^{T_{Σ}(V)}(a_{1}, …, a_{n})].

T_{0} induces a congruence relation on T_{Σ}(V) as follows:

Definition 3.12. For s, t ∈ T_{Σ}(V), let s ≡_{T_{0}} t iff 1. s, t ∈ T_{Σ_{0}}(V_{0}) and T_{0} ⊧ s = t or

2. s = t = x for an extended variable x ∈ V ∖ V_{0} or

3. s = f(s_{1}, …, s_{k}) and t = f(t_{1}, …, t_{k}) for some operation symbol f : w → s in Σ ∖ Σ_{0} and tuples (s_{1}, …, s_{k}), (t_{1}, …, t_{k}) ∈ (T_{Σ}(V))^{w} such that s_{i} ≡_{T_{0}} t_{i} for all i = 1, …, k.

T_{0} can be enriched with the uninterpreted symbols of Σ ∖ Σ_{0} giving rise to a new theory T_{0}^{=}, such that T_{0}^{=} ⊧ s = t iff s ≡_{T_{0}} t.

Lemma 3.13 ([AR93]). ≡_{T_{0}} is a congruence relation on T_{Σ}(V).

Proof. This is easily proved by induction on the height of terms. For further details see [AR93]. □ ✓

Henkin’s version of the proof of Gödel’s completeness theorem extends T_{0} to a maximal consistent theory and enlarges it by adding formulae of the form ∃xP (x) ⇒ P (c), where c is a new constant symbol called a witness of ∃xP (x). Following Henkin’s approach, the subsequent assumptions are presumed:

Assumption 3.14 (on the built-in theory and signature). T_{0} is a complete theory and for every formula of the form ∃xP (x) there is a ground term t in T_{Σ_{0}}(∅) such that T_{0} ⊧ ∃xP (x) ⇒ P (t).

If T_{0} satisfies the above assumption then it is called a Henkin theory.

Remark 3.15. First of all, note that a complete theory is maximal consistent and all its models are elementary equivalent. Considering only complete theories is not a strong restriction since, usually, basic theories are understood as theories of a specific model. In particular, the examples of basic theories considered in this work, PAR and SA, are complete.

As was mentioned in example 3.4, the constants …, −1, 0, 1, … constitute the ground terms of the built-in language which give the universe of the models of interest. The method of construction of witnessing constants for a firstorder language is a well-known way to expand the built-in language in order to obtain the required expressiveness. For the models of interest of the usual built-in theories (SA, PAR, etc.), it is always possible to give a signature with a ground term for any element of the universe. For example, with explicit constants …, −1, 0, 1, … or with functions ‘s’ for successor, ‘p’ for predecessor and constant ‘0’. ◁

The preceding lemma gives rise to the construction of a Σ-algebra over T_{0}.

Lemma 3.16 ([AR93]). Under the above assumption, T_{Σ}(V)/ ≡_{T_{0}} is a Σalgebra over T_{0}.

Proof. (Sketch) The carrier of T_{Σ}(V)/ ≡_{T_{0}} consists of the S-sorted set of equivalence classes of terms in T_{Σ}(V) with respect to the congruence relation ≡_{T_{0}}. Functions and predicates are interpreted according to representatives of equivalence classes. Because of completeness of T_{0} and by induction on the structure of formulae it can be proved that the basic model of T_{Σ}(V)/ ≡_{T_{0}} is also a model of the basic theory. For further details see [AR93]. □ ✓

Remark 3.17. In order to obtain from T_{Σ}(V) (and the congruence ≡_{T_{0}}) a Σalgebra over T_{0}, T_{0} should be a complete theory. In effect, suppose that T_{0} is the (one-sorted) basic theory of Σ_{0} (the language which consists of a predicate symbol p and two constant symbols a, b) axiomatized by the sentence p(a)∨p(b). By definition of the interpretation of predicate expressions, p(a) and p(b) do not hold in T_{Σ}(V) since T_{0} |̸= p(a) and T_{0} |̸= p(b), respectively. Therefore the single axiom of T_{0} does not hold in T_{Σ}(V). Contrarily, if T_{0} is assumed to be complete, then either T_{0} ⊧ p(a) or T_{0} ⊧ p(b) (or both), which implies that the interpretation of predicate expressions in T_{Σ}(V) satisfies p(a)∨p(b). ◁

Now, implications with built-in premises are defined.

Definition 3.18. Let (Σ, Σ_{0}, T_{0}) be a signature. A universal Horn clause of the form:

∀X(t_{1} = t′_{1} ∧ ⋯ ∧ t_{k} = t′_{k} ∧ P ⟹ t_{0} = t′_{0}),

where, for i = 0, …, k, t_{i}, t′_{i} are S-sorted extended terms of the same sort and P is a built-in predicate, is called a universal Horn clause with built-in predicate P over the theory T_{0}. The built-in predicate P is often called built-in condition. t_{0} = t′_{0} is called the conclusion and t_{1} = t′_{1} ∧ ⋯ ∧ t_{k} = t′_{k} is called the standard condition of the clause.

Definition 3.19. Let Φ ≡ ∀X(t_{1} = t′_{1} ∧ ⋯ ∧ t_{k} = t′_{k} ∧ P ⟹ t_{0} = t′_{0}) be a universal Horn clause with built-in predicate and let � be an algebra over the built-in theory T_{0}. An assignment α : X → A satisfies Φ iff its homomorphic extension, denoted also by α : T_{Σ}(X) → A, satisfies α(t_{0}) = α(t′_{0}) whenever α(t_{m}) = α(t′_{m}) for m = 1, …, k and 𝔄 satisfies P with assignment α (denoted also by 𝔄_{α} ⊧ P). Φ is said to be valid in an algebra � if all assignments α : X → A satisfy Φ. This is denoted by � ⊧ Φ.

Given a set H of universal Horn clauses with built-in predicates over the theory T_{0}. The class of all algebras over T_{0} which validate all clauses in H is denoted by Mod_{T_{0}} H. Mod_{T_{0}} H is called the universal Horn class of H over the built-in theory T_{0}. Mod_{T_{0}} H is said to be axiomatized by H and the clauses in H are said to be the axioms of Mod_{T_{0}} H.

A class K of algebras over T_{0} is said to be a universal Horn class over the built-in theory T_{0} if K = Mod_{T_{0}} H for some set H of universal Horn clauses with built-in predicates over T_{0}.

A clause Φ is said to be a logical consequence of H if for every algebra � ∈ Mod_{T_{0}}H, � ⊧ Φ. This is denoted by H ⊧_{T_{0}} Φ (or simply by H ⊧ Φ when there is no confusion).

As usual, � ⊧_{T_{0}} H means that � ∈ Mod_{T_{0}}H.

Example 3.20. Consider the signature of arrays presented in example 3.4. The following set of universal Horn clauses with built-in predicates over the Presburger arithmetic (PAR) defines a universal Horn class over PAR.

∀i, j, A, L (i =_{PAR} j ⟹ ⟨A, i, L⟩[j] = L).
∀i, j, A, L (i < j ∨ j < i ⟹ ⟨A, i, L⟩[j] = A[j]).
∀i, j, A, L, K (i =_{PAR} j ⟹ ⟨⟨A, i, K⟩, j, L⟩ = ⟨A, j, L⟩).
∀i, j, A, L, K (¬(i =_{PAR} j) ⟹ ⟨⟨A, i, K⟩, j, L⟩ = ⟨⟨A, j, L⟩, i, K⟩).
∀i, j, k, A, L, K (¬(i =_{PAR} j) ⟹ ⟨⟨A, i, K⟩, k, L⟩[j] = ⟨A, k, L⟩[j]).

i, j, k are (built-in) variables of sort int, A and L, K of sort array and element, respectively. The formula i =_{PAR} j is an abbreviation for i < j +1 & j < i+1. Conditions of the fourth and fifth rules illustrate inequalities in the built-in language (this is not really necessary because PAR ⊧ i ≠ j ⇔ (i < j ∨ j < i)).

Note that universal Horn clauses as well as universal Horn clauses with built-in predicates admit only positive equalities as standard conditions. The intended semantics of ⟨A, i, L⟩ is the array A replacing its i-th element with L. The intended semantics of A[i] is the i-th element of the array A. ◁

Remark 3.21. The previous example appears to be non satisfactory because it does not combine built-in predicates and equations (as conditions). A more elaborated example, extension of the present one, combining equations and built-in predicates, in order to extend an order on the objects of the array sort to an order on the arrays is presented in [AR93]. So, it can be observed that in this sense the present approach is effectively superior to the use of constraints.

◁

It remains to examine closure properties and algebraic characterizations of universal Horn classes over built-in theories, as is done for varieties and quasivarieties. As previously mentioned, subalgebras can be defined restricting the basic model of every subalgebra to remain identical to the original Σ-algebra. For this notion of subalgebra, one can reply the classical proof of closure under subalgebras for varieties and quasivarieties. Universal Horn classes over built-in theories are a generalization of universal Horn classes because universal Horn classes over the empty theory are precisely the second ones.

4. Calculus for universal Horn clauses with built-in predicates

A set of inference rules for universal Horn clauses with built-in predicates is introduced and its completeness is proved. Freeness notions for universal Horn clauses with built-in predicates are presented.

The following assumption is given to make decidability of built-in predicates effective.

Assumption 4.1 (on the basic theories). Only basic theories whose set of quantifier-free logical consequences, T h^{∀}(T_{0}) =^{def} {P | T_{0} ⊧ P, P is quantifier-free}, is decidable will be considered.

Definition 4.2. Let H be a set of universal Horn clauses with built-in predicates over a theory T_{0}. Consider the set of inference rules of Table 1. Deductions are finite sequences of universal Horn clauses with built-in predicates called formal proofs leading from the given set H to another clause Φ, the conclusion of the deduction. Clauses occurring in a formal proof are either in H or else can be inferred from earlier ones of the sequence by one of the inference rules. Φ is said to be deducible from H if there is a deduction from H whose last clause Rules of congruence: \overline{∀X(P)}, P ∈ T h^{∀}(T_{0}), X ⊇ var(P). \overline{∀X(s=t)}, s ≡_{T_{0}} t, X ⊇ var(s) ∪ var(t). \overline{∀X(t=t′ ⟹ t′=t)}. \overline{∀X(t=t′ ∧ t′=t′′ ⟹ t=t′′)}. \overline{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n} ⟹ f(... ,t_{1},... ,t_{n},...)=f(... ,t′_{1},... ,t′_{n},...))}, ∀f in Σ ∖ Σ_{0}.

Rules of closure: \overline{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t_{1}=t′_{1})}, n ≥ 1.

\frac{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P_{1} ⟹ t=t′)}{∀X(t_{1}=t′_{1}∧···∧t_{n+k}=t′_{n+k}∧(P_{1}&P_{2}) ⟹ t=t′)}, k, n ≥ 0, (P_{2} empty implies k > 0).

\frac{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P_{1} ⟹ t_{0}=t′_{0}),∀X(t_{0}=t′_{0}∧t_{n+1}=t′_{n+1}∧···∧t_{n+k}=t′_{n+k}∧P_{2} ⟹ t=t′)}{∀X(t_{1}=t′_{1}∧···∧t_{n+k}=t′_{n+k}∧(P_{1}&P_{2}) ⟹ t=t′)}, k, n ≥ 0.

\frac{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P_{2} ⟹ t=t′)}{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P_{1} ⟹ t=t′)}, P_{1} ⇒ P_{2} ∈ T h^{∀}(T_{0}), n ≥ 0.

\frac{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t=t′)}{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n} ⟹ t=t′)}, P ∈ T h^{∀}(T_{0}), n ≥ 0. \overline{∀X((¬P) ⟹ t=t′)}, P ∈ T h^{∀}(T_{0}), X ⊇ var(P) ∪ var(t) ∪ var(t′).

Rule of full invariance: \frac{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t=t′)}{∀Y (σ(t_{1})=σ(t′_{1})∧···∧σ(t_{n})=σ(t′_{n})∧σ(P) ⟹ σ(t)=σ(t′))}, ∀σ : X → T_{Σ}(V),

Y = ⋃_{x∈X} var(σ(x)), n ≥ 0.

Rules of conjunction: \frac{∀X(t_{1}=t′_{1}∧t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t=t′)}{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t=t′)}, n ≥ 1.

\frac{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t=t′)}{∀X(t_{ϕ(1)}=t′_{ϕ(1)}∧···∧t_{ϕ(n)}=t′_{ϕ(n)}∧P ⟹ t=t′)}, ∀ϕ permutation of \{1, …, n\} (n ≥ 2).

Rule of abstraction: \frac{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t=t′)}{∀Y (t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t=t′)}, where n ≥ 0 and Y = X ∪ \{y\} for y ∈ V ∖ X.

Rule of concretion: \frac{∀X(t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t_{0}=t′_{0})}{∀Y (t_{1}=t′_{1}∧···∧t_{n}=t′_{n}∧P ⟹ t_{0}=t′_{0})}, where n ≥ 0 and Y = X ∖ \{x\},

for x ∈ X ∖ (⋃_{i=0}^{n} var(t_{i} = t′_{i}) ∪ var(P)), X_{s} ≠ ∅ ⟹ T_{Σ}(Y)_{s} ≠ ∅, ∀s ∈ S.

Table 1. Inference rules for universal Horn classes with built-in predicates. is Φ. This is denoted by H ⊢_{T_{0}} Φ (or when no confusion can arise simply by H ⊢ Φ).

Remark 4.3. The first rule of congruence allows generalization of quantifierfree logical consequences of the built-in theory, i.e. valid built-in predicates. Note that formulae of the form ∀X(P) are not universal Horn clauses with builtin predicates. This rule makes sense due to the assumption of decidability of T h^{∀}(T_{0}).

Note that the second rule of congruence trivially implies ∀X(t = t). The fifth rule of congruence should be more precisely interpreted as

∀X(t_{1} = t′_{1} ∧ ⋯ ∧ t_{n} = t′_{n} ⟹

f(s_{1}^{0}, …, s_{k_{0}}^{0}, t_{1}, …, t_{n}, s_{1}^{n}, …, s_{k_{n}}^{n}) = f(s_{1}^{0}, …, s_{k_{0}}^{0}, t′_{1}, …, t′_{n}, s_{1}^{n}, …, s_{k_{n}}^{n})),

where the terms t_{i}, t′_{i} for 1 ≤ i ≤ n are extended terms and the terms s_{j}^{i} for 0 ≤ i ≤ n, 1 ≤ j ≤ k_{i} are basic ones. By abuse of notation, if k_{i} = 0 for some i = 0, …, n then the corresponding sequence of basic arguments, s_{1}^{i}, …, s_{k_{i}}^{i}, is considered empty.

The sixth rule of closure allows deduction of universal Horn clauses with T_{0}-inconsistent built-in predicates. In fact, P T_{0}-inconsistent means that any model of T_{0} does satisfy P. Therefore, for all models 𝔄 of T_{0}, 𝔄 ⊧ ¬P which means that T_{0} ⊧ ¬P. ◁

There exists a smallest congruence relation on T_{Σ}(V) generated by the set of universal Horn clauses H which includes ≡_{T_{0}}. This congruence will be used to prove the completeness theorem.

Definition 4.4. Let:

• ≡_{H,T_{0}}^{0} = ≡_{T_{0}}

• ≡_{H,T_{0}}^{i+1} is defined as the smallest congruence on T_{Σ}(V) which includes ≡_{H,T_{0}}^{i} and such that for all clauses ∀Y (t_{1} = t′_{1} ∧ ⋯ ∧ t_{n} = t′_{n} ∧ P ⟹ t = t′) in H and all assignments α : Y → T_{Σ}(V) if α(t_{i}) ≡_{H,T_{0}}^{i} α(t′_{i}) for all i = 1, …, n and T_{0} ⊧ α(P) then α(t) ≡_{H,T_{0}}^{i+1} α(t′).

Finally, ≡_{H,T_{0}} is defined as ⋃_{i≥0} ≡_{H,T_{0}}^{i}.

Observe that ≡_{H,T_{0}} can also be conceived as the smallest congruence over the Σ-algebra T_{Σ}(V)/ ≡_{T_{0}} generated by H, since the ≡_{H,T_{0}}^{i} congruences, for i ≥ 1, do not change the congruence classes of basic sorts. Therefore it makes sense to speak of the congruence ≡_{H} over T_{Σ}(V)/ ≡_{T_{0}}. Obviously, ≡_{H,T_{0}} is the smallest congruence on T_{Σ}(V) generated by H which contains ≡_{T_{0}}. In effect, by definition ≡_{T_{0}} is contained in ≡_{H,T_{0}} and for all clauses ∀Y (t_{1} = t′_{1} ∧ ⋯ ∧ t_{n} = t′_{n} ∧ P ⟹ t = t′) in H and all assignments α : Y → T_{Σ}(V) if α(t_{i}) ≡_{H,T_{0}} α(t′_{i}) for all i = 1, …, n and T_{0} ⊧ α(P) then exists k such that α(t_{i}) ≡_{H,T_{0}}^{k} α(t′_{i}) for all i = 1, …, n and by definition α(t) ≡_{H,T_{0}}^{k+1} α(t′) which implies that α(t) ≡_{H,T_{0}} α(t′).

A freeness notion for universal Horn classes with built-in predicates is examined before the completeness proof.

Results about freeness and initiality of T_{Σ}(V)/ ≡_{H} and T_{Σ}/ ≡_{H} for the multi-sorted case (when T_{0} is the empty theory) can be found in [Kap83] and [Cla88]. These results cannot directly be applied for the case of universal Horn clauses with built-in predicates because T_{Σ}(V)/ ≡_{H,T_{0}} carries the semantics of the built-in theory T_{0}.

First of all, recall that only complete theories are considered. Usually one works with a special model of the theory, for example for the case of the AN T only the standard model and its isomorphisms are considered, i.e., the model over the structure of the natural numbers with the usual addition and successor.

In the following two theorems Mod_{T_{0}}H is restricted to the subclass of Σalgebras whose reduct with respect to the basic part (Σ_{0}) is a term generated model of T_{0} (see [Gal87] for definitions). This subclass of Σ-algebras is called basic-term generated algebras of Mod_{T_{0}}H. In a basic-term generated algebra � of Mod_{T_{0}}H, every function and every predicate symbol in Σ_{0} receive an interpretation in 𝔄. In particular, the standard models of SA and AN T are term generated (in effect, the interpretations 0^{𝔄}, s(0)^{𝔄}, s(s(0))^{𝔄}, … represent all possible elements of an standard model 𝔄 of SA and AN T ).

Theorem 4.5 (Construction of free algebras, [AR93]). T_{Σ}(V)/ ≡_{H,T_{0}} is free over V in the subclass of basic-term generated algebras of Mod_{T_{0}}H.

Proof. (Sketch) To see that T_{Σ}(V)/ ≡_{H,T_{0}}∈ Mod_{T_{0}}H, observe that lemma 3.16 and the fact that ≡_{H,T_{0}} does not change the congruence classes of basic terms of ≡_{T_{0}} imply that T_{Σ}(V)/ ≡_{H,T_{0}} is a Σ-algebra over T_{0}. Let ∀X(t_{1} = t′_{1} ∧⋯∧t_{n} = t′_{n} ∧P ⟹ t = t′) be a clause in H and α : X → T_{Σ}(V)/ ≡_{H,T_{0}} be an arbitrary assignment and suppose that its homomorphic extension, de noted also by α : T_{Σ}(X) → T_{Σ}(V)/ ≡_{H,T_{0}}, satisfies α(t_{i}) = α(t′_{i}) for all i = 1, …, n and T_{0} ⊧ α(P). Let nat : T_{Σ}(V) → T_{Σ}(V)/ ≡_{H,T_{0}} be the natural application from terms into its corresponding equivalence classes with respect to ≡_{H,T_{0}}. Since nat is surjective there exists h : X → T_{Σ}(V) such that its homomorphic extension, denoted also by h : T_{Σ}(X) → T_{Σ}(V), satisfies α = itnat ∘ h. Then nat(h(t_{i})) = nat(h(t′_{i})) for all i = 1, …, n. Therefore h(t_{i}) ≡_{H,T_{0}} h(t′_{i}). By construction of ≡_{H,T_{0}} and since T_{0} ⊧ h(P), there exists k such that h(t_{i}) ≡_{H,T_{0}}^{k} h(t′_{i}) for all i = 1, …, n. Consequently h(t) ≡_{H,T_{0}}^{k+1} h(t′) which implies that α(t) = nat(h(t)) = nat(h(t′)) = α(t′).

To prove that for all basic-term generated algebras � of Mod_{T_{0}}H and arbitrary assignments α : V → A there exists a unique β : T_{Σ}(V)/ ≡_{H,T_{0}}→ A such that β∘nat = α steps of freeness p roof in [EM85] could be followed making appropriate considerations on ≡_{T_{0},H}. For further details see [AR93]. □ ✓

Theorem 4.6 ([AR93]). Let ∀X(t = t′) be a purely equational clause which holds in the Σ-algebra T_{Σ}(X)/ ≡_{H,T_{0}}. Then for all basic-term generated algebras � of Mod_{T_{0}}H, � ⊧ ∀X(t = t′).

Proof. Let α : X → A be an arbitrary assignment and α : T_{Σ}(X) → A denote also its homomorphic extension. By the previous theorem, there exists exactly a homomorphism β : T_{Σ}(X)/ ≡_{H,T_{0}}→ A, such that α = beta ∘ nat, where nat : T_{Σ}(X) → T_{Σ}(X)/ ≡_{H,T_{0}} is the natural application from terms into its corresponding equivalence classes with respect to ≡_{H,T_{0}}.

Validity of ∀X(t = t′) in T_{Σ}(X)/ ≡_{H,T_{0}} implies nat(t) = nat(t′) and then β(nat(t)) = β(nat(t′)). Thus α(t) = α(t′). Therefore � ⊧ ∀X(t = t′). □ ✓

Remark 4.7. In the preceding two theorems the essential restriction of Mod_{T_{0}}H to basic-term algebras allows a treatment of Σ-homomorphisms similar to the classical one in the algebraic context. In a certain sense, this restriction can be thought as a type of initial property for the basic theory, since only Σ-algebras whose basic part is a standard model generated by the language of Σ_{0} are admitted. To illustrate precisely the above situation, consider Mod_{SA}H (without the mentioned restriction), where the basic theory is SA, the extension Σ ∖ Σ_{0} is composed by two constant symbols a, b : → s and a function symbol f : nat → s, where nat is the sort of SA and s is a new sort and H is the following set of clauses:

\begin{matrix}f(0) = a; \\ ∀x(f(x) = a ⇒ f(s(x)) = a). \end{matrix}

Note that the equation ∀x(f(x) = a) does not hold in Mod_{SA}H since there exists a nonstandard model (of SA) which satisfies f(x) = a for all x ∈ IN and f(x) = b for all x ∉ IN. Therefore H |̸= ∀x(f(x) = a). However, note that T_{Σ}(V)/ ≡_{H,T_{0}}⊧ ∀x(f(x) = a). On the other hand, H ⊬ ∀x(f(x) = a), since the induction schema of SA does not apply for the whole extended language (viz, a, b, f ∈ Σ ∖ Σ_{0}).

In the case of PAR the situation is more complex because induction is equivalent to the well-ordering property for integers, namely, that every nonempty set of integers with a lower bound has a least element. ◁

The completeness proof of the inference rules is resumed with The following simple lemma.

Lemma 4.8. Let H be a set of universal Horn clauses. Let C and P be respectively any fixed standard condition and built-in predicate. Let ∼_{C,P} be defined as t ∼_{C,P} t′ iff H ⊢ ∀X(C ∧ P ⟹ t = t′). Then ∼_{C,P} is an equivalence relation.

Theorem 4.9 (Completeness). Let H be a set of universal Horn clauses with built-in predicates over a theory T_{0}. An arbitrary universal Horn clause Φ with built-in predicates over T_{0} is a logical consequence of H if and only if Φ is deducible from H. In symbols:

H ⊧ Φ iff H ⊢ Φ.

Proof. (Sketch) Soundness of the calculus can easily be showed for each rule, as usual.

Conversely, to prove that H ⊧ Φ ⟹ H ⊢ Φ, let C = s_{1} = s′_{1}∧⋯∧s_{k} = s′_{k} be any standard condition with terms in T_{Σ}(X) and let P be any T_{0}-consistent built-in predicate with terms in T_{Σ_{0}}(X_{0}), where X_{0} denotes the basic variables of X. Note that by the sixth rule of closure it is enough to consider T_{0}- consistent built-in predicates. sk(t) denotes the term t considering the variables of X as constants. Let �_{X,C∧P} be the quotient algebra T_{Σ}(X)/ ≡_{H̃,T̃_{0}}, where H̃ = H ∪ sk(C) and T̃_{0} = T_{0} ∪ {sk(P)}. Note that to speak of T_{Σ}(X) with the semantics of T_{0} ∪ {sk(P)} makes sense, because for a quantifier-free formula Φ in T_{Σ_{0}}(X_{0}) one can decide if T_{0} ⊧ sk(P) ⇒ Φ and this is equivalent to T_{0} ∪ {sk(P)} ⊧ Φ by the well known deduction theorem. The definition of ≡_{H̃,T̃_{0}} is analogous with the one of ≡_{H,T_{0}}.

It is enough to prove that �_{X,C∧P} ⊧ sk(t) = sk(t′) implies H ⊢ ∀X(C ∧ P ⟹ t = t′). In effect, assume that this holds and suppose that for every algebra � ∈ Mod_{T_{0}}H, � ⊧ ∀X(C ∧ P ⟹ t = t′). Then in particular �_{X,C∧P} ⊧ ∀X(C ∧ P ⟹ t = t′) and, by definition of �_{X,C∧P}, �_{X,C∧P} ⊧ sk(C) ∧ sk(P) which implies �_{X,C∧P} ⊧ sk(t) = sk(t′). Then by assumption H ⊢ ∀X(C ∧ P ⟹ t = t′). Note that �_{X,C∧P} is effectively an algebra in Mod_{T_{0}}H: by lemma 3.16 and since P is T_{0}-consistent, T_{Σ}(V)/ ≡T̃_{0} is a Σ-algebra over T_{0}; by definition of ≡_{H,T_{0}} and in particular of ≡_{H̃,T̃_{0}}, �_{X,C∧P} validates all the clauses in H.

A family of congruences similar to ≡_{H,T_{0}}^{i} is built in order to prove that �_{X,C∧P} ⊧ sk(t) = sk(t′) implies H ⊢ ∀X(C ∧ P ⟹ t = t′).

Let ≡_{0}^{C∧P} be the smallest congruence on T_{Σ}(X) (which in this case carries the semantics of T̃_{0}) which contains ≡T̃_{0} and sk(C) and such that for all purely equational clauses ∀Y (u = u′) ∈ H and all assignments α : Y → T_{Σ}(X), sk(α(u)) ≡_{0}^{C∧P} sk(α(u′)).

≡_{i+1}^{C∧P} is recursively defined as the smallest congruence on T_{Σ}(X) which includes ≡_{i}^{C∧P} and such that for all universal Horn clauses ∀Y (t_{1} = t′_{1} ∧ ⋯ ∧ t_{n} = t′_{n} ∧ Q ⟹ t = t′) in H and all assignments α : Y → T_{Σ}(X), if T_{0} ⊧ sk(P) ⇒ sk(α(Q)) and sk(α(t_{i})) ≡_{i}^{C∧P} sk(α(t′_{i})) for all i = 1, …, n then sk(α(t)) ≡_{i+1}^{C∧P} sk(α(t′)).

Finally, ≡^{C∧P} = ⋃_{i≥0} ≡_{i}^{C∧P}. To conclude it, it is sufficient to prove that for all i ≥ 0, sk(t) ≡_{i}^{C∧P} sk(t′) implies H ⊢ ∀X(C ∧ P ⟹ t = t′). This results from a relatively simple inductive proof.

\underline{i=0}: By the lemma 4.8 and fifth rule of congruence it is enough to prove that H ⊢ ∀X(C ∧ P ⟹ α(t) = α(t′)) for all equations ∀Y (t = t′) in H ∪ sk(C) and all assignments α : Y → T_{Σ}(X).

First, suppose that ∀Y (t = t′) ∈ H. By the rule of full invariance H ⊢ ∀X(α(t) = α(t′)) and by the second rule of closure H ⊢ ∀X(C ∧ P ⟹ α(t) = α(t′)). Second, let s_{j} = s′_{j} ∈ C (for some 1 ≤ j ≤ k). By the first rule of closure H ⊢ ∀X(C ∧ P ⟹ s_{j} = s′_{j}).

\underline{i}: Suppose that sk(t) ≡_{i}^{C∧P} sk(t′) implies H ⊢ ∀X(C ∧ P ⟹ t = t′).

\underline{i+1}: Again, by lemma 4.8 and the fifth rule of congruence it is enough to prove that H ⊢ ∀X(C ∧ P ⟹ α(t) = α(t′)) for all universal Horn clauses ∀Y (t_{1} = t′_{1} ∧ ⋯ ∧ t_{n} = t′_{n} ∧ Q ⟹ t = t′) in H and all assignments α : Y → T_{Σ}(X) such that sk(α(t_{j})) ≡_{i}^{C∧P} sk(α(t′_{j})) holds for all j = 1, …, n and T_{0} ⊧ sk(P) ⇒ sk(α(Q)).

By the rule of full invariance, H ⊢ ∀X(α(t_{1}) = α(t′_{1}) ∧ ⋯ ∧ α(t_{n}) = α(t′_{n}) ∧ α(Q) ⟹ α(t) = α(t′)). By induction hypothesis H ⊢ ∀X(C∧P ⟹ α(t_{j}) = α(t′_{j})) for all i = 1, …, n. Applying repeatedly the third rule of closure and the rules of conjunction, it can be obtained H ⊢ ∀X(C ∧ (P &α(Q)) ⟹ α(t) = α(t′)). Note also that T_{0} ⊧ P ⇒ α(Q) results trivially as a generalization of T_{0} ⊧ sk(P) ⇒ sk(α(Q)) because in a given model 𝔄 of T_{0} with universe A any interpretation of the constant symbols of sk(P) (i.e. of the basic variables of X considered as constants) is permissible. Finally, by applying the fourth rule of closure to H ⊢ ∀X(C ∧ (P &α(Q)) ⟹ α(t) = α(t′)) and the fact that T_{0} ⊧ P ⇒ (P &α(Q)) (which results trivially from T_{0} ⊧ P ⇒ α(Q)) it is obtained H ⊢ ∀X(C ∧ P ⟹ t = t′). □ ✓

5. Conclusions

Conditional equational specifications and built-in predicates or constraints in a many-sorted first-order theory were carefully combined. This amalgamation of algebraic structures and logical theories is useful in the fields of algebraic specification and term rewriting but it is usually treated without giving enough attention to the related formal problems. In fact, some algebraic properties such as freeness and the simple notion of initial algebra cannot naturally be inherited from purely conditional equational specifications, as it is frequently assumed. Here special and appropriate notions and restrictions on the built-in predicates and on the conditional equational specifications were developed guaranteeing the basic algebraic properties needed in order to obtain a complete deductive calculus for this class of combined specifications.

In order to make the process of deduction effective, standard conditional rewriting techniques and built-in decision algorithms should appropriately be combined. Appropriate notions of standard conditional term rewriting systems with built-in predicates appear in [AR97] where it was reported on a complete algorithm based on conditional term rewriting and built-in decision algorithms for effective deduction of formulae of the form P ⟹ s = t, where P is a pure built-in premise. The author presents also proofs of Newman’s diamond lemma and the Church-Rosser property for the corresponding class of combined term rewriting systems in [AR98].

Acknowledgements. The author would like to thank Claus-Peter Wirth and Klaus Madlener for their valuable suggestions and comments which have improved his early conception of this work and Rodolfo Baigorri for his corrections and remarks.

References

[AB92] J. Avenhaus and K. Becker, Conditional rewriting modulo a built-in algebra, SEKI-Report SR-92-11, Fachbereich Informatik, Universität Kaiserslautern, Postfach 3049, D-67653 Kaiserslautern (Germany), 1992.

[AR93] M. Ayala-Rincón, Expressiveness of Conditional Equational Systems with Builtin Predicates, Ph.D. thesis, Universität Kaiserslautern, Kaiserslautern (Germany), December 1993.

[AR94] M. Ayala-Rincón, Confluence of Conditional Rewriting Systems with Built-in Predicates and Standard Premises as Conditions, XXI Seminário Integrado de Software e Hardware, Caxambú, Brazil, August 1994, pp. 507–521.

[AR95] M. Ayala-Rincón, A Deductive Calculus for Conditional Equational Systems with Built-in Predicates as Premises — Extended Abstract —, XV International Conference of the Chilean Computer Science Society, Arica, Chile, November 1995, pp. 25–36.

[AR97] M. Ayala-Rincón, A Decision Procedure for Conditional Rewriting Systems with Built-in Predicates, XXIV Seminário Integrado de Software e Hardware, Brasília, Brazil, August 1997, pp. 387–398.

[AR98] M. Ayala-Rincón, Church-Rosser Property for Conditional Rewriting Systems with Built-in Predicates as Premises, Second Frontiers of Combining Systems, Amsterdam, Holland, Applied Logic Series, Kluwer Academic Publishers, October 1998, To appear.

[ARG97] M. Ayala-Rincón and L. M. R. Gadelha, Some Applications of (Semi-)Decision Algorithms for Presburger Arithmetic in Automated Deduction based on Rewriting Techniques, La Revista de La Sociedad Chilena de Ciencia de la Computación 2 (1997), no. 1, 14–23.

[Bec94] K. Becker, Rewrite Operationalization of Clausal Specifications with Predefined Structures, Ph.D. thesis, Universität Kaiserslautern, Kaiserslautern (Germany), April 1994.

[CK90] C. C. Chang and H. J. Keisler, Model Theory, third ed., Studies in Logic and the Foundation of Mathematics, vol. 73, North-Holland Publishing Company, 1990.

[Cla88] I. Classen, Algebraische Grundlagen der Termersetzung mit bedingten Gleichungen, Tech. Report 88-04, TU Berlin, 1988, In German.

[Coo72] D. C. Cooper, Theorem Proving in Arithmetic without Multiplication, Machine Intelligence 7 (1972), 91–99.

[DO90] N. Dershowitz and M. Okada, A Rationale for Conditional Equational Programming, Theoretical Computer Science 75 (1990), 111–138.

[EM85] H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification 1, EATCS Monographs on Theoretical Computer Science, Springer, 1985.

[Gal87] J. H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, John Wiley & Sons, Inc., 1987.

[Kap83] S. Kaplan, Un langage de Spécification de types abstraits algébriques, Ph.D. thesis, Universite de Paris-Sud Centre D’Orsay, February 1983, In French.

[Kap84] S. Kaplan, Conditional Rewrite Rules, Theoretical Computer Science 33 (1984), 175–193.

[KKR90] Claude Kirchner, Hélène Kirchner, and M. Rusinowitch, Deduction with Symbolic Constraints, Revue d’Intelligence Artificielle 4 (1990), no. 3, 9–52, Special issue on Automatic Deduction.

[O’D77] M. J. O’Donnell, Computing in Systems Described by Equations, LNCS, vol. 58,

Springer, 1977.

[Pad88] P. Padawitz, Computing in horn clause theories, EATCS Monographs on Theoretical Computer Science, Springer, 1988.

[Pre29] M. Presburger, Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, 1. Kongres matematyków krajow slowiańskich, Warsaw, 1929, in German, pp. 92–101.

[Sho81] R. E. Shostak, Deciding Linear Inequalities by Computing Loop Residues, Journal of the Association for Computing Machinery 28 (1981), no. 4, 769–779.

[Vor89] S. G. Vorobyov, Conditional rewrite rule systems with Built-in Arithmetic and Induction, Proc. Third Int. Conference on Rewriting techniques and Applications, Chapel-Hill, NC (N. Dershowitz, ed.), LNCS, vol. 355, Springer, April 1989, pp. 492–512.

[Wec92] W. Wechler, Universal algebra for computer scientists, EATCS Monographs on Theoretical Computer Science, Springer, 1992.

(Recibido en abril de 1996, revisado en noviembre de 1997)

Departamento de Matemática

Universidade de Brasília 70900-010 Brasília DF, BRASIL

e-mail: ayala@mat.unb.br