OI-implication: Soundness and Refutation Completeness

1 Introduction

Logical implication, as a relationship on clausal spaces, is particularly hard to handle due to many negative results descending from its non-decidability [Schmidt-Schauss, 1988] and intrinsic complexity [Gottlob and Ferm¨ uller, 1993]. This is the reason why subsumption, being more tractable and efficiently implementable than stronger relationships (i.e., relationships that entail it), is the generalization model commonly exploited in Inductive Logic Programming (ILP).

Attempts have been made to weaken subsumption and implication in order to obtain more manageable ordering relationships between clauses. Consider, for instance, forms of non-decreasing subsumption such as the weak subsumption [Badea and Stanciu, 1999], or weaker but decidable forms of implication such as T-implication [Idestam-Almquist, 1995]. Indeed, the algebraic structure of the search space, and hence the refinement operators that can be defined, are affected by the choice of the underlying ordering relationship.

Weakening implication by assuming the object identity bias allowed for the definition of OI-implication, a novel relationship between clauses which makes the search space more manageable [Esposito et al., 2000]. Specifically, it has been possible to prove the existence of ideal refinement operators for the search spaces ordered by the resulting form of logical implication, while this is not possible in standard clausal spaces [Nienhuys-Cheng and de Wolf, 1997]. This is particularly important for the efficiency of the refinement in search spaces with dense solutions [Badea and Stanciu, 1999]. Indeed, it has been shown as the computational complexity of the resulting operators is much more appealing than the one of the refinement operators defined for other search spaces.

Furthermore, the object identity framework for machine learning has been also exploited in the definition of operators performing inductive learning as well as abstraction and abduction, so to have a unique knowledge representation and reasoning framework for multistrategy learning.

In this paper, a proof-theoretic definition is adapted from [Esposito et al., 2000] and a new model-theoretic definition of the implication under object identity is introduced. These definitions are shown to be equivalent. Indeed, two main results are demonstrated, namely the soundness of the derivation procedure compliant with the assumption of the mentioned bias and a subsumption theorem which allows for the demonstration that this procedure is also refutation-complete.

These results open new directions for the investigation of other interesting properties of this form of implication, such as the proof of a compactness theorem, the decidability and all the other algebraic properties of the search space, ordered by the relationship induced by this form of implication.

This paper is organized as follows. In Section 2, a semantics is defined, complying with the object identity assumption; hence, the definition of OI-implication is presented together with the proof of the soundness of the related proof procedure. Refutation completeness through the Subsumption Theorem, are proven in Section 3. Section 4 draws the conclusions of this research, outlining the ongoing developments.

2 OI-implication

In our framework, we adopt a representation language L expressing theories as logic programs made up of clauses. The basic notions about clausal representation can be found in [Lloyd, 1987; Nienhuys-Cheng and de Wolf, 1997].

The framework we propose relies essentially on the following assumption, which is commonly employed. For instance, defining the concept of bicycle, one would mention the two wheels among its components. Then, in order to rule out an instance of a different concept such as a monocycle, the identification of the two wheels should be avoided (a bicycle is two-wheeled by definition).

A thorough treatment of these issues for the Datalog clausal language is offered in [Semeraro et al., 1998]. We want to extend this to a more expressive clausal language, without the restriction to function-free terms. In our setting we want to avoid the identification of terms.

Assumption 2.1 (Object Identity) In a clause, terms denoted with different symbols must be distinct, i.e. they represent different entities of the domain.

This notion can be viewed as an extension of Reiter's unique names assumption [Reiter, 1980]. Object identity is the basis for the definition of both an equational theory for the language clauses and a quasi-order upon them.

This assumption brings to a modified equational theory consisting in the addition of one axiom to an Equality Theory [Lloyd, 1987], namely:

for all pairs (t1, t2) of distinct terms occurring in a clause.

Nienhuys-Cheng and de Wolf have embedded an equality theory in the semantics, for demonstrating the completeness of the SLDNF resolution, when dealing with the completion of normal programs, yielding the so called E-Herbrand interpretations [Nienhuys-Cheng and de Wolf, 1997]. Badea and Stanciu, in the definition of the weak subsumption [1999], deal with substitutions which do not identify literals. In this paper, we adopt a different approach, founded on a semantic basis. A similar approach to capturing the object identity assumption can be considered that of the unique substitution semantics [Khardon, 1999].

2.1 Semantics andModel-Theoretic Definition

Some definitions follow, specifying how the object identity assumption changes the semantics for the clausal representation. We start off by defining the relation between the terms of the language and the domain we deal with.

A pre-interpretation J under object identity of a first-order language is exactly a standard pre-interpretation:

• A non-empty set D called the domain of the preinterpretation;
• Each constant in L is assigned to an element of D;
• Each n-ary function symbol f is assigned a mapping Jf from Dn to D.

Then, we need to map variables (and terms) to the objects of the domain:

Definition 2.1 Let J be a pre-interpretation of L with domain D. A variable assignment under object identity V w.r.t. L is a one-to-one mapping from the variables of L to the domain D of J. We use V (X/d) to denote that the variable X is mapped to d ∈ D in the variable assignment V , and the other variables are mapped according to V . The term assignment under object identity Z in a formula φ w.r.t. J and V of terms in L is the following mapping from the terms in L to D:

1. J maps each constant to an element of D;
2. V maps each variable to a distinct element of D;
3. If d1, . . . , dn are the elements of D to which the terms t1, . . . , tn are mapped, then the term f(t1, . . . , tn) is mapped to Jf(d1, . . . , dn), where Jf is the function from Dn to D assigned to the function symbol f by J, s.t. ∀t1, t2 ∈ terms(φ) : Z(t1/d1),Z(t2/d2) implies d1 ̸= d2.

By combining pre-interpretations and variable (term) assignments, we can specify the notion of interpretation under object identity:

Definition 2.2 Given J a pre-interpretation of L with domain D, an interpretation I under object identity (OIinterpretation) based on J assigns a mapping IP from Dn to {T, F} to each predicate symbol P .

Given a variable assignment under object identity V , be Z the corresponding term assignment w.r.t. J and V . Then a formula φ in L has a truth value under I defined as follows:

1. For each atom A = P(t1, . . . , tn), if ∀i = 1, . . . , n : di ∈ D is assigned to ti by Z, then the truth value of A under I and V is IP (d1, . . . , dn);
2. The truth values of the formula φ obtained by using connectives is determined using the standard truth tables.
3. If φ = ∃Xψ then φ has truth value T under I and V if there exists d ∈ D for which ψ has truth value T under I and V (X/d), where V (X/d) is a legal variable assignment under object identity. Otherwise, φ has truth value F under I and V .
4. If φ = ∀Xψ then φ has truth value T under I and V if for all elements d ∈ D ψ has truth value T under I and V (X/d), where V (X/d) is a legal variable assignment under object identity. Otherwise, φ has truth value F under I and V .

The standard notions of tautology, contradiction, satisfiability and consistency can be straightforwardly extended to the new semantics.

In ILP we focus our interest on clauses. Since they are closed formulas, the truth values do not depend on variable assignments. We can represent an interpretation as a set of ground literals, i.e. those that are true according with the interpretation.

Definition 2.3 Given a closed formula φ, an OIinterpretation I is called a model under object identity (OI-model) for φ iff I satisfies φ. Given a set of closed formulas Σ, I is an OI-model for Σ iff it is an OI-model for all formulas φ ∈ Σ.

OI-interpretations are always standard interpretations. Conversely, we show with an example a case when an OImodel for a formula is not a model.

Example 2.1 Let C = p(X) ∨ p(a). An OI-model for C, assumed the domain is D = {a, b}, is represented by the Herbrand OI-interpretation I = {p(b)}.

I is not a model for C in the standard meaning. Indeed, since p(a) is stated as false, the truth of the clause depends on p(X), where variable X is universally quantified. Under object identity, it is sufficient that p(b) be true for ∀Xp(X) to hold. The same does not apply in the standard semantics where both p(a) and p(b) should be true.

We are now ready to define the form of implication that is compliant with the object identity assumption:

Definition 2.4 Given a set of formulas Σ and a formula φ, Σ OI-implies φ or φ is a logical consequence under object identity of Σ (denoted with Σ|=OIφ) iff all OI-models I of Σ are OI-also models of φ.

Thus, useful results hold also in this semantics:

Theorem 2.1 (Deduction Theorem) Let Σ be a set of formulas and φ and ψ be formulas. Then Σ ∪ {φ}|=OIψ iff Σ|=OI (φ → ψ).

Proof. Σ ∪ {φ}|=OIψ iff all OI-models of Σ ∪ {φ} are OI-models of ψ iff all OI-models of Σ are OI-models of ¬φ or of ψ iff all OI-models of Σ are OI-models of ¬φ ∨ ψ iff Σ|=OI (φ → ψ).

As a consequence, it is possible to prove also this result:

Theorem 2.2 Let Σ be a set of formulas and φ be a formula. Then Σ|=OIφ iff Σ ∪ {¬φ} is unsatisfiable.

Proof. Σ|=OIφ iff (by Theorem 2.1) Σ ∪ {¬φ}|=OI ✷ iff all OI-models of Σ ∪ {¬φ} are OI-models of ✷ iff Σ ∪ {¬φ} is unsatisfiable under object identity.

As concerns clauses, in the standard semantics it is possible concentrate the interest on Herbrand models only [Lloyd, 1987], This can be extended to our setting.

Proposition 2.3 Let Σ be a set of clauses in a first order language L. Then Σ has an OI-model iff Σ has an Herbrand OI-model.

Proof.

• (⇒) Suppose Σ has an OI-model I. Then we define the Herbrand OI-interpretation I with:
• the same pre-interpretation of I and having as domain the Herbrand universe UL;
• Let P an n-ary predicate symbol occurring in Σ. Then we define the function IP from UL to {F, T} as follows: IP (t1, . . . , tn) = T if P(t1, . . . , tn) is true under I and IP (t1, . . . , tn) = F otherwise.

(⇐) Obvious.

2.2 Proof-Theoretic Definition and Soundness

Given a notion of subsumption under object identity, and using a subsumption theorem, we define implication under object identity proof-theoretically. The goal here is to define this relationship in a constructive way.

First, we have to define a form of resolution coping with the object identity assumption. To this purpose, we discuss some further properties required to substitutions in order to fulfill this assumption. In fact, a substitution can be regarded as a function mapping variables to terms. Hence, we require these functions to satisfy certain additional properties in order to preserve object identity.

Definition 2.5 Given a set of terms T, a substitution σ is an OI-substitution w.r.t. T iff ∀t1, t2 ∈ T : t1 ̸= t2 implies t1σ ̸= t2σ.

In the following, we will omit the set of terms T when it is obvious. Based on OI-substitutions, it is possible to define other related notions such as the composition of OIsubstitutions, ground and renaming OI-substitutions, as well as instance clauses, ground clauses and variants.

In order to cope with the object identity assumption, a new relationship has been derived [Semeraro et al., 1998] from the classic θ-subsumption. Its definition can be given by exploiting the notion of OI-substitution [Esposito et al., 2000].

Definition 2.6 Let C and D be two clauses. Then, C θOI-subsumes D iff there exists σ, an OI-substitution w.r.t. terms(C), such that Cσ ⊆ D.

The notion of θOI-subsumption induces a quasi-order upon the space of clauses [Semeraro et al., 1998]. Besides, a notion of equivalence for θOI-subsumption can be defined, that partitions the space of clauses in equivalence classes. Since θOI-subsumption maps each literal of the subsuming clause onto a single literal in the subsumed one, equivalent clauses under θOI-subsumption must have the same number of literals. Thus, a search space ordered by θOI-subsumption is made up of non-redundant clauses. This yields smaller equivalence classes than those in a space ordered by θ-subsumption.

Now, as we have done for the substitutions, we can specify a notion of a unifier fulfilling Assumption 2.1:

Definition 2.7 Given a finite set of simple expressions S, we say that θ is an OI-unifier iff ∃E ∀Ei ∈ S : Eiθ = E and θ is an OI-substitution w.r.t. terms(Ei). An OI-unifier θ for S is called a most general OI-unifier (mguOI) for S iff, for each OI-unifier σ of S, there exists an OI-substitution τ such that σ = θτ .

In this setting, clauses cannot have proper subsets as factors. Hence, this notion can be used only for standardizing apart the variables of the parent clauses before a step of resolution [Esposito et al., 2000].

Definition 2.8 Given the clauses C and D, suppose they are standardized apart. A clause R is an OI-resolvent of C and D iff, there exist M ⊆ C and N ⊆ D such that {M,N} is unifiable through the mguOI θ and

This definition of OI-resolution follows Robinson's original definition [Robinson, 1965]. However, a different definition has been given, based on the one given in [Chang and Lee, 1973], taking into account one complementary pair of literals for each resolution step [Esposito et al., 2000].

Definition 2.9 Let T be a set of clauses. The OI-resolution closure of T, denoted by R∗OI (Σ), is defined inductively:

If there exists an OI-derivation of C from Σ, this will be denoted with Σ⊢OIC which is equivalent to C ∈ R∗OI (Σ).

It is interesting to consider also the case of linear resolution [Chang and Lee, 1973], which was originally exploited for the proof-theoretic definition of OI-implication [Esposito et al., 2000]. If C can be derived by means of zero or more linear OI-resolution steps from the set of clauses Σ, we denote this with C ∈ LnOI (Σ), n > 0, where LOI denotes the linear OI-resolution operator and L∗OI stands for its closure.

In order to prove the soundness of the proof-procedure defined above, some preliminary results are needed.

Lemma 2.4 Let C1 and C2 be clauses. If there exists R that is the OI-resolvent of C1 and C2 then it holds {C1, C2}|=OIR.

Proof. Assume that the two clauses are standardized apart. Suppose R is an OI-resolvent of C1 and C2, resolved upon the subsets of literals M and N, and let θ be the mguOI(M,N) employed. Suppose the OI-interpretation I with domain D is an OI-model for {C1, C2}.

Let {X1, . . . ,Xn} = vars(C1) ∪ vars(C2) and V be a variable assignment under object identity. Then, ∀i = 1, . . . , n, di ∈ D if Mθ is false under I and V (X1/d1) · · · (Xn/dn), at least one of the other literals in C1 is true under I and V (X1/d1) · · · (Xn/dn). Similarly for N. Note that R is made up of all literals in C1θ and C2θ except Mθ or Nθ.

Since either Mθ or Nθ is false under I and V (X1/d1) · · · (Xn/dn), at least one of the literals in R is true under I and V (X1/d1) · · · (Xn/dn), hence I is an OI-model of R. Therefore, {C1, C2}|=OIR.

This result can be inductively extended to OI-derivations, proving the soundness of OI-resolution:

Theorem 2.5 (Soundness) Let Σ be a set of clauses, and C be a clause. If Σ⊢OIC then Σ|=OIC.

Proof. Suppose Σ⊢OIC. Then there exists an OI-derivation R1, . . . , Rk = C from Σ. By induction on k, it holds:

• (k = 1) R1 = C ∈ Σ, thus obviously Σ|=OIC.

(k > 1) Suppose the thesis holds for m ≤ k.

Let R1, . . . ,Rk+1 = C be an OI-derivation of C from Σ. If Rk+1 ∈ Σ then the theorem is obvious. Otherwise, Rk+1 is an OI-resolvent of some Ri and Rj (i, j ≤ k). By the inductive hypothesis, we have Σ|=OIRi and Σ|=OIRj. From Lemma 2.4, it follows that {Ri, Rj}|=OIRk+1 = C.

Now we can give a proof-theoretic definition of the notion of OI-implication. In the next section, we will justify this formally, showing the equivalence of the two versions.

Definition 2.10 Let C and D be two clauses. Then C implies D under object identity (C OI-implies D), denoted C ⇒OI D iff either D is a tautological clause or there exists a clause E ∈ R∗OI ({C}) such that E θOI-subsumes D. Equivalence under OI-implication is denoted by ⇔OI.

From the definition above, it is easy to see that OIimplication is a strictly a stronger ordering relationship than θOI-subsumption. Moreover the set of most specific clauses ⊥ will be made up by tautologies.

We will prove in the next section that Definitions 2.4 and 2.10 are equivalent, by means of a subsumption theorem.

3 Refutation Completeness

The soundness theorem for OI-implication bridges the gap from the proof-theoretic to the model-theoretic definition of this notion. In this section we give a proof of a completeness result to make the same step in the other direction. Following the proof-schema given in [Nienhuys-Cheng and de Wolf, 1996] for the standard case, first we prove this result for ground clauses, then we lift it to the general case.

3.1 Preliminaries

Let us start from the simplest case when both Σ and C are ground.

Lemma 3.1 Let Σ be a logic program of ground clauses and C be a ground clause. If Σ|=OIC then there exists D such that Σ⊢OID and D ⊆ C.

The proof is almost the same as in the case of standard implication (see [Nienhuys-Cheng and de Wolf, 1996]) since no variable assignment is made, for the clauses are ground. Yet in our case we considered finite sets of clauses. This can be extended by means of a compactness theorem.

In order to prove the Subsumption Theorem when only clause C is required to be ground, we need two theorems that are valid for the notion of unsatisfiability for standard interpretations but can be proven also when the object identity is assumed.

Theorem 3.2 A set of clauses Σ is unsatisfiable under object identity iff there exists a finite unsatisfiable set Γ of ground instances of clauses from Σ.

See [Nienhuys-Cheng and de Wolf, 1997] for a proof for standard interpretations. In this setting, it comes by using Proposition 2.3.

From this result and the Deduction Theorem another result follows:

Theorem 3.3 Let Σ be a non-empty set of clauses and C be a ground clause. Then Σ|=OIC iff there exists a finite set Γ of ground instances of clauses from Σ such that Γ|=OIC.

Again, see [Nienhuys-Cheng and de Wolf, 1997] for a proof in the standard case. In this setting, Theorems 2.1 and 3.2 are to be exploited.

Now we have to show how to lift an OI-resolution step from the case of ground parent clauses to that of unrestricted clauses.

Lemma 3.4 Let C1 and C2 be two clauses and C′1 and C′2 , respectively, two instances of them. If R′ is an OI-resolvent of C′1 and C′2 , then there exists a clause R, that is an OIresolvent of C1 and C2, such that R′ is an instance of R.

Proof. Suppose that C1, C2, C′1 and C′2 are standardized apart. Be σ1,2 the OI-substitutions such that C′1 = C1σ1 and C′2 = C2σ2.

Now let D′1 = C′1 \N ′1 and D′2 = C′2 \N ′2 for some D1 ⊂ N1 and D2 ⊂ N2. Hence, R′ = (D′1 ∪D′2 )µ = (D1σ1∪D2σ2)µ. Since the clauses are standardized apart, we can write: R′ = (D1 ∪ D2)σ1σ2µ.

Let N ′1 ⊆ C′1 and N ′2 ⊆ C′2 be the subsets of literals resolved upon for obtaining R′ , then there exist N1 ⊆ C1 and N2 ⊆ C2 such that N ′1 = N1σ1 and N ′2 = N2σ2. Suppose that µ be an mguOI(N ′1 , N ′2 ).

Consider N1 and N2. They can be unified through the OIunifier σ1σ2µ. Then, let θ be an mguOI(N1,N2), there exists an OI-substitution δ such that σ1σ2µ = θδ.

Thus, C1 and C2 can be resolved under object identity upon N1 and N2 by using θ: R = ((C1\N1)∪(C2\N2))θ = (D1∪ D2)θ. Then Rδ = (D1 ∪ D2)θδ = (D1 ∪ D2)σ1σ2µ = R′ . Hence R′ = Rδ.

We can generalize the lifting technique to the case of OIderivations, i.e. to multiple OI-resolution steps.

Lemma 3.5 Let Σ be a finite set of clauses and Σ′ a set of instances of clauses from Σ. Suppose that R′1 , . . . ,R′k be an OI-derivation of clause R′k from Σ′ . Then there exists an OIderivation R1, . . . ,Rk of clause Rk from Σ such that R′i is an instance of Ri, for each i = 1, . . . , k.

Proof. By induction on the length of the derivation k.

• (k = 1) In this case R′1 ∈ Σ′ . But Σ′ is made up of instances of the clauses in Σ. Hence, ∃R1 ∈ Σ such that R′1 is an instance of R1.
• (k > 1) By hypothesis, let us suppose the thesis proven up to a derivation of length m. We have to prove it for

k = m + 1. Let R′1 , . . . ,R′m+1 be an OI-derivation of R′m+1 from Σ′ , so that R′m+1 is the resolvent of two clauses in Σ′ ∪ {R′1 , . . . , R′m}. By hypothesis, there exists an OI-derivation R1, . . . , Rm of Rm from Σ such that ∀i = 1, . . . ,m : R′i is an instance of Ri. Hence, by Lemma 3.4, there exists Rm+1 such that R′m+1 is one of its instances.

We have now all the instruments for proving the following result:

Lemma 3.6 Let Σ be a finite set of clauses and C be a ground clause. If Σ|=OIC then there exists D such that Σ⊢OID and D ⊆ C.

Proof. Assume that C is not a tautology. We look for a clause D fulfilling the thesis. From Σ|=OIC and Theorem 3.3, then there exists a finite set Σg such that each clause in Σg is a ground instance of a clause in Σ and Σg|=OIC.

Then, from Lemma 3.1 there exists a clause D′ such that Σg⊢OID′ and D′ ⊆ C. Let R′1 , . . . ,R′k = D′ be an OIderivation of D′ fromΣg.

By means of Lemma 3.5, the OI-derivation can be lifted to an OI-derivation R1, . . . ,Rk of Rk from Σ, where D′ = R′k is an instance of Rk. Let D = Rk. Then Σ⊢OID and D θOIsubsumes C (since D′ = Dδ and D′ ⊆ C).

3.2 Subsumption Theorem and Consequences

Preliminarily, we have to recall the notion of a particular substitution that will be used in the next proofs:

Definition 3.1 Let Σ be a set of clauses and C be a clause. Let {X1, . . . ,Xn} = vars(C) and suppose we have a set of constants {a1, . . . , an} ∩ consts(Σ ∪ C) = ∅. Then σ = {X1/a1, . . . , Xn/an} is a Skolem substitution for C w.r.t. Σ.

This notion is easily extensible to this setting, it is easy to see that Skolem substitutions are also OI-substitutions.

Now, given the results of the previous sections, we can prove the main result and some consequences.

Theorem 3.7 (Subsumption Theorem) Let Σ be a finite set of clauses and C be a clause. Then Σ|=OIC iff there exists a clause D such that Σ⊢OID and D θOI-subsumes C.

Proof.

• (⇒) Assume that C is not a tautology. Let θ be a Skolem OIsubstitution for C w.r.t. Σ. Then Cθ is a ground clause which is not a tautology and Σ|=OICθ.

By Lemma 3.6, there is a clause D such that Σ⊢OID and D θOI-subsumes Cθ. Since D is derived from Σ, D cannot contain constants yielded by θ. Therefore θ maps variables of C to constants that are not in D.

• Let δ be an OI-substitution such that D θOI-subsumes Cθ and σ be the OI-substitution obtained by replacing each binding Xi/ti in δ with Xi/ai. Then δ = σθ. Since θ only replaces the variables Xi by ai (1 ≤ i ≤ n), it follows that Dσ ⊆ C. Then D θOI-subsumes C. Hence, the thesis holds.
• (⇐) For the soundness of the OI-derivation (and θOIsubsumption).

As a consequence of this theorem, similarly to the standard case, it is nearly straightforward to demonstrate some important results originally due to Gottlob [1987].

Definition 3.2 A clause C is ambivalent when there are two literals L1,L2 ∈ C with the same predicate symbol but opposite sign. Besides, if they unify then the clause C is called recursive.

Of course only unification through OI-substitutions is taken into account here. Given these notions, it is possible to show when OI-implication and θOI-subsumption coincide:

Proposition 3.8 Let C and D be clauses. If C is not recursive and D is not tautological, then C|=OID iff C θOIsubsumes D.

Proof. Assume that C|=OID. By Theorem 3.7 it holds that ∃E ∈ R∗OI ({C}): E θOI-subsumes D. Since C is not recursive {C} = R∗OI ({C}). Hence, C θOI-subsumes D. The (⇐) part is obvious.

Now, given a clause C, we denote with C+ and C-, respectively, the set of its positive and negative literals.

Proposition 3.9 Let C andD be clauses. If C|=OID then C+ θOI-subsumes D+ and C- θOI-subsumes D-.

Proof. Observe that C+ θOI-subsumes C then C +|=OIC. By the hypothesis, it holds: C|=OID, thus C+|=OID. Note that by construction C+ and D+ contain only positive literals, then C + cannot be OI-resolved with itself, and D+ is not a tautology. By Proposition 3.8, it must hold that C+ θOIsubsumes D.

Again, observing that C+ is made up of positive literals only, one can conclude that C+ θOI-subsumes D+.

Analogously C- θOI-subsumes D-.

This property can be used for the proof of the decidability of the implication under object identity. Yet, this subject goes beyond the scope of this paper.

Finally, we state a sufficient condition for the equivalence to hold between OI-implication and θOI-subsumption:

Proposition 3.10 Let C and D be clauses. If D is not ambivalent, then C|=OID iff C θOI-subsumes D.

Proof. Assume C|=OID and D non ambivalent. Thus D cannot be a tautology.

• By Proposition 3.9 it holds C+θ ⊆ D+ and C -δ ⊆ D- for some OI-substitutions θ and δ.

Now, if C were recursive then there would be a literal L = Lσ1 = Lσ2 such that Lσ1 ∈ C+ and ¬Lσ2 ∈ C-, with σ1 and σ2 OI-unifiers. But then Lσ1θ ∈ D+ and ¬Lσ2δ ∈ D-, which does not hold since D is not ambivalent.

• Thus C is not recursive and D is not tautological. By Proposition 3.8, it follows that C θOI-subsumes D.

The Subsumption Theorem showed that OI-resolution, together with θOI-subsumption, can derive the same conclusions drawn model-theoretically by implication under object identity. In standard implication, resolution is not deduction complete (some θ-subsumption steps could be needed), yet it might be complete with respect to an unsatisfiable set of clauses. We prove this result in the object identity setting.

Theorem 3.11 (Refutation Completeness) Let Σ be a finite set of clauses. Then Σ is unsatisfiable under object identity iff Σ⊢OI✷.

Proof.

• (⇒) Be Σ a finite set of clauses such that Σ|=OI ✷. For the Subsumption Theorem 3.7, there exists D such that Σ⊢OID and D θOI-subsumes ✷. Then D must be the empty clause itself. Hence Σ⊢OI✷
• (⇐) For the soundness of the OI-derivation (Theorem 2.5).

All the theorems and propositions of the previous section can be extended to the case of an infinite set of formulas Σ if a Compactness Theorem like that for standard models [Boolos and Jeffrey, 1989] can be demonstrated. Yet, here we are interested in these issues concerning logic programs, hence finite sets of clauses only.

4 Conclusions and FurtherWork

A framework has been presented for the novel notion of implication under object identity. By assuming this bias over a clausal representation, we were able to define OI-implication both model-theoretically and proof-theoretically. The two definitions can be unified by exploiting the soundness of the OI-derivations and a subsumption theorem which is the basis for proving the refutation completeness of our procedure. This relationship, that is stronger than θOI-subsumption, induces a quasi-order over the clausal search space conferring different algebraic properties than standard implication.

We expect encouraging results on the complexity of learning/revising logic theories in such a search space. Hence, from a theoretical viewpoint, we are now concerned with the demonstration of the compactness and decidability of this new relationship. Another research stream will concern the algebraic properties of the resulting search space. In particular, algorithms for calculating minimal generalizations and specializations are to be developed.

In a more long term perspective, we aim at building an integrated framework for multistrategy learning that will benefit by these theoretical findings.