Spaces of Theories with Ideal Refinement Operators

1 Motivation

In the investigation of the algorithms for relational learning, regarding induction as a refinement process allows to decou­ ple search from heuristics. Therefore, the choice of the gen­ eralization model for a search space plays a key role since it affects both its algebraic structure and the definition of refine­ ment operators for that space.

Logical implication and B-subsumption are the relation­ ships that are commonly employed for inducing generaliza­ tion models in relational learning (the latter turning out to be more tractable with respect to the former). Yet, they are not fully satisfactory because of the complexity issues that the resulting search spaces present, although subspaces have been found where the generalization model is more manage­ able. Indeed, the effectiveness and efficiency of learning as a refinement process strongly depends on the properties of the search space and, as a consequence, of the operators. In some cases the important property to be required to operators is .flexibility [Badea, 2001], meaning that they should be ca­ pable of focussing dynamically on certain zones of the search space that may be more promising. Conversely, the property of ideality [Nienhuys-Cheng and de Wolf, 1997] has been rec­ ognized as particularly important for the efficiency of incre­ mental algorithms in search spaces with dense solutions. It is also possible to derive non-redundant operators from ideal ones, the former being more suitable for spaces with rare so­ lutions [Badea and Stanciu, 1999].

Most algorithms for relational learning, such as those employed in FOIL [Quinlan, 1990] and PROGOL [Muggleton, 1995], adopt iterative covering strategies, separate­ and-conquer [Fiimkranz, 1999], based on the refinement of clauses. Alternative methods are based on divide-and­ conquer strategies [Bostrom and Asker, 1999]. Although these refinements may tum out to be optimal with respect to a single clause, the result of assembling them in a theory is not guaranteed to be globally effective, since the interde­ pendence of the clauses with respect to covering may lead to better theories made up of locally non-optimal clauses. Only some systems, e.g. MPL [De Raedt eta!., 1993] or HYPER [Bratko, 1999], cope with the problem ofleaming whole the­ ories rather than constructing them clause by clause.

This urges more complex refinement operators to be adopted in algorithms obeying to a different strategy that is able to take into account the possible interactions between the single clausal refinements. Hence, the new problem is defining operators that refine whole theories rather than single clauses [Midelfart, 1999; Badea, 2001]. ALEPH is a system where ideas on theory-level induction has been rudimentarily implemented [Srinivasan, 2002] . Of course, heuristics are re­ quired to cope with the combinatorial complexity of the prob­ lem. The resulting extended setting would also take into ac­ count background knowledge that may be available, and then it is also comparable to generalized and relative subsump­ tion [Plotkin, 1971; Bun tine, 1988] or implication [Nienhuys­ Cheng and de Wolf, 1997].

Weakening implication by assuming object identity, an ex­ tension of the unique names assumption [Reiter, 1980], as a semantic bias has led to the definition of 001-subsumption and Of-implication [Esposito eta!. , 200lb], clausal relation­ ships which induce more manageable search spaces. The ex­ istence of ideal refinement operators in these generalization models is possible [Esposito eta!., 2001a], while this does not hold in clausal spaces ordered by B-subsumption or impli­ cation [Nienhuys-Cheng and de Wolf, 1997]. The objective of this work is to extend the results obtained for spaces of clauses and prove the existence of ideal refinement operators for spaces of theories in those generalization models.

This paper is organized as follows. In Section 2, we recall semantics and proof-theory adopted in the framework. Sec­ tion 3 deals with refinement operators and their properties. Then, in Section 4, the operators for the search space consid­ ered are defined and proven to be ideal. Section 5 summarizes the paper outlining possible developments.

2 Generalization Models and Object Identity

The representation language adopted in the proposed frame­ work concerns logic theories (whose space is denoted 2c) made up of clauses (space C). The background notions about clausal representations in Inductive Logic Programming can be found in [Nienhuys-Cheng and de Wolf, 1997].

The framework relies essentially on the following bias pro­ posed in [Esposito eta!. , 200lb]:

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

The intuition is the following: in spaces based on general­ ization models induced by B-subsumption (or implication), considered the two clauses C = q(x ) ,_ p(X, X) and D = q(x ) ,_ p(X, X) ,p(X, Y),p(Y, Z) ,p(Z, X), they tum out to be equivalent (in fact C is the reduced clause of D); this is not so natural as it may appear, since more elements of the domain can be accounted for in D than in C (indeed in this framework C is more general than D). The expressive power is not diminished by this bias, since it is still possi­ ble to convey the same meaning of a clause, although em­ ploying more clauses, e.g. when object identity is assumed, q(X) ,_ p(X, Y) is equivalent to the pair of clauses (a the­ ory) {(q(X) ,_ p(X,X)), (q(X) ,_ p(X, Y))}.

Now it has to be specified how this bias affects the seman­ tics and proof theory of a clausal representation.

2.1 Proof Theory and Semantics

Starting from substitutions, we recall the specification of the proof theory under object identity. Since a substitution can be regarded as a mapping from the variables to the terms of a language, we require these functions to satisfy additional properties to avoid the identification of terms:

Definition 2.1 Given a set of terms T (omitted when ob­ vious), a substitution a is an 01-substitution w.r.t. T iff Vt1 , t2 E T: t1 =f. t2 implies t1 a =f. t2a.

Based on Or-substitutions, it is possible to define related no­ tions such as ground and renaming or-substitutions, their composition and also unification:

Definition 2.2 Given a finite set of clauses S, we say that B is an or-unifier iff3E such that 1::/ Ei E S : EiB = E and B is an Of-substitution w.r.t. terms(Ei)·

An Of-unifier B for Sis a most general 01-unifierfor S iff for each Of-unifier a of S there exists an Of-substitution T such that a = Br. This is denoted with mgUo1 (S) .

The following notions represent resolution and derivation when exclusively 01-unifiers are used.

Definition 2.3 Given the clauses C and D that are supposed standardized apart, a clause R is an 01-resolvent ofC and D iff there exist M ~ C and N ~ D such that { M , N} is unifiable through the mgu01 B and R E ( ( C \ M) U ( D \ N)) B. R 01 (C, D) is the set of the 01-resolvents ofC and D.

An Of-derivation is obtained by successively chaining or­ resolutions.

Definition 2.4 Given a theory T, the closure ofOI-resolution is recursively defined: n~,(T) = Un>O n~,(T), with n g,(T) = T and n~,(T) = n~,- 1 (T) u {R = nOI(C, D) I C, DE R~,- 1 (T)}.

If3C E R~ 1 (T) then there is an or-derivation ofC from T of length n.

With respect to the model theory under object identity, more specific models are needed:

Definition 2.5 Given a non-empty domain V, a pre­ interpretation J of the language C assigns each constant to a different element ofV and each n-ary function symbol f to a mapping from vn to V .

An Or-interpretation I based on J is a set of ground instances of atoms with arguments mapped in V through J.

Given a ground Of-substitution 1 mapping vars(C) to V, an instance A y of an atom A is true in I iff Ar E I otherwise it is false in I . A negative literal ·Ar is true in I iff Ar is not, otherwise it is false in I.

I is an or-model for the clause C iff for all ground Of­ substitutions 1 there exists at least a literal in Cr that is true in I , otherwise the clause is false in I .

Hence, the form of implication that is compliant with this se­ mantics has been defined [Esposito eta!. , 200lb] which, in tum, induces a quasi-order on spaces of clauses and theories.

Definition 2.6 Let C, D be two clauses. C implies D under object identity (and then Cis more general than D w.r.t. Of­ implication) iff all Of-models for C are also Of-models for D. This relationship is denoted with Cf=o,D.

Analogously, a theory T implies C under object identity, de­ noted with Tf=o1C, iff all Of-models forT are also Of-models for C. Finally, a theory T is more general than a theory T' w.r.t. Of-implication iffi::/C' E T': Tf=o,C'.

or-implication is a constrained form oflogical implication biased by the object identity assumption, as shown in the fol­ lowing example:

Example 2.1 Given the two theories T = {(p(X) ,_ q(f(X) , Y) , q(Y, f(X))) , (q(f(X) , j(X)) ,_ r(Z))} and T' = {p(X) ,_ r(Z)}, observe that T I= T' butT ;f=o,T'. This depends on the disallowed binding Y / f (X) that would identify terms within the same clause.

The proof-procedure was proven sound in [Esposito et a!., 200lb], thus bridging the gap from the proof-theory to the model-theoretic definition of 01-implication.

2.2 ~:ll-subsumption and 01-implication

A simpler syntactic relationship, that is B-subsumption biased by the object identity assumption, has been defined based the notion of or-substitution.

Definition 2. 7 Given two clauses C and D, C tb1-subsumes D iff there exists an Of-substitution a w.r.t. terms( C) such that Ca ~ D. In this case, Cis more general than D w.r.t. tb1-subsumption, denoted C?:01D. If also D?n1C then they are equivalent w.r.t. {b1-subsumption, denoted C"'b1D.

Analogously, given the theories T, T', Tis more general than T' w.r.t. {b1-subsumption iffi::/D E T' 3C E T: C?n1D, denoted T?n1 T'.

This quasi-order is weaker than OI-implication as proven by the following result [Esposito eta!., 200lb]:

Theorem 2.1 Given a theory T and a non-tautological clause C, Tf=01C if/3D E R~1 (T) such that D?:n1C.

This result bridges the gap from model-theory to proof­ theory. It also suggests the way to decompose OI-implication that is exploited for defining complete refinement operators.

Similarly to standard implication, it is nearly straightfor­ ward to demonstrate some consequences of Theorem 2.1 originally due to Gottlob [1987]. Given a clause C, let c+ and c- denote, respectively, the sets of its positive and neg­ ative literals. Then, it holds:

Proposition 2.1 Let C and D be clauses. JfCf=01D then c+ f.bJ-subsumes D+ and c- 8o1-subsumes D- .

Since OI-substitutions map different literals of the sub­ suming clause onto different literals of the subsumed clause, equivalent clauses under ea,-subsumption have the same num­ ber of literals. Thus, a space ordered by 8o1-subsumption is made up of non-redundant clauses. Indeed, it holds:

Proposition 2.2 Let C and D be two clauses. If C Bo1subsumes D then ICI ~ IDI. Moreover, c"tJ,D if! they are alphabetic variants.

As a consequence of the propositions above, it is possi­ ble to prove the following results giving lower bounds for the depth and cardinality of clauses in the generalization model based on OI-implication [Fanizzi and Ferilli, 2002].

Definition 2.8 The depth of a term t is 1 when t is a vari­ able or a constant. Jft = j(t1, ... , tn). then depth(t) = 1 + max~1 (depth( ti) ). The depth of a clause C, denoted depth( C), is the maximum depth among its terms.

Proposition 2.3 Given the clauses C and D, ifCf=o,D then it holds that depth( C)~ depth(D) and ICI ~ IDI.

3 Theory Refinement and Object Identity

A learning problem can be cast as a search problem [Mitchell, 1982] where theory refinement is triggered when new evi­ dence made available is to be assimilated. The canonical in­ ductive paradigm requires the fulfillment of the properties of completeness and consistency for the synthesized theory with respect to a set of input examples. When an inconsistent (re­ spectively, incomplete) hypothesis is detected, a specializa­ tion (resp., generalization) of the hypothesis is required in order to restore this property of the theory. In the former case the refinement operators must search the space looking for more specific theories (downward refinements); in the latter, more general theories (upward refinements) are required.

The formal definition of the refinement operators for generic search spaces, is based on the algebraic notion of a quasi-ordered set S that is a set endowed with an ordering relationship (say :::S) that is reflexive and transitive.

Definition 3.1 Given a quasi-ordered set (S, :::S). a refine­ ment operator is a mapping from S to 2 5 such that:

• vc E s: p(C) <;;;;{DEs I D :::S C} (downward refinement operator)
• vc E s: o(C) <;;;;{DEs 1 c:::; D} (upward refinement operator)

A notion of closure upon refinement operators is required when proving the completeness of the operators.

Definition 3.2 In a quasi-ordered set (S, :::S). letT be are­ finement operator. The closure ofT for C E S is recursively defined: T*(C) = Un>O Tn(C). where T 0 (C) = {C} and Tn(C) ={DES I 3E E Tn-l(C): DE T(E)}.

Ultimately, refinement operators should construct chains of refinements, i.e. a sequence C0 , C1, ... , Cn of elements of S such that ci E T(Ci-1), 1 ~ i ~ n going from the starting elements to target ones.

3.1 Properties of the Refinement Operators

As mentioned above, the properties of the refinement opera­ tors depend on the algebraic structure of the search space. A refinement operator traverses a refinement graph in the search space, that is a directed graph containing an edge from T to T' inS in case the operator Tis such that T' E T(T) .

A major source of inefficiency may come from refinements that turn out to be equivalent to the starting ones. Depend­ ing on the search algorithm adopted, computing refinements that are equivalent to some element that has been already dis­ carded may introduce a lot of useless computation. As to the effectiveness of the search, a refinement operator should be able to find a path between any two comparable elements of the search space (or their equivalent representatives). It is de­ sirable that at least one path in the graph can lead to target el­ ements. This means that a complete refinement operator can derive any comparable element in a finite number of steps. The following properties formally define these concepts:

Definition 3.3 In a quasi-ordered set (S, :::S). a refinement operator T is locally finite if! 'riC E S : T( C) is finite and computable.

A downward (resp. upward) refinement operator p (resp. o) is proper iff'r/C E S : D E p(C) implies D ~ C (resp. DE o(C) implies C ~D).

A downward (resp. upward) refinement operator p (resp. o) is complete if! 'riC, D E S , D ~ C implies 3E E S : E E p*(C) and E "' D (resp. C ~ D implies 3E E S: E E o*(C) and E"' D).

Let us observe that local finiteness and completeness en­ sure the existence of a computable refinement chain to a tar­ get element, and properness ensure a more efficient refine­ ment process, by avoiding the search of equivalent clauses. Then, the combination of these properties confers more ef­ fectiveness and efficiency to an operator:

Definition 3.4 In a quasi-ordered set (S, :::S). a refinement operator is ideal iff it is locally finite, proper and complete.

As mentioned in the introduction, other important proper­ ties of refinement operators have been defined, yet they go beyond the scope of this paper which focusses on ideality.

3.2 Minimal Refinements of Clauses

The existence of maximal specializations and minimal gener­ alizations of clauses was proven for both the ea,-subsumption and the OI-implication generalization model [Fanizzi and Ferilli, 2002]. These results are briefly recalled here for be­ ing used in the construction of ideal refinement operators pre­ sented in the following section.

As a consequence of Theorem 2.1, some limitations are provable as concerns depth and cardinality for a clause that implies (subsumes) another clause under object identity. This yields a bound to the proliferation of possible generalizations:

Proposition 3.1 Let C and D be two clauses. The set of gen­ eralizations ofC and D w.r.t. Of-implication is finite.

The proof is straightforward since the depths and cardinalities of the generalizations are limited as a consequence of Propo­ sition 2.3. Now, given two clauses C and D, Jet G be the set of generalizations of { C, D} w.r.t. 01-implication. Observe that G =1- 0 since D E G. Proposition 3.1 yields that G is finite. Thus, since the test of 01-implication between clauses is decidable [Fanizzi and Ferilli, 2002], it is theoretically pos­ sible to determine the minimal elements of G by comparing the clauses in G and eliminating those that are overly general.

For computing theories that are proper generalizations of the starting ones, an operator for inverting 01-resolutions is needed which is similar to the V-operator for the inversion of resolution [Muggleton, 1995]:

Definition 3.5 Given a theory T, the operator for the inver­ sion of the OI-resolution is defined:

Note that there is a Jot of indeterminacy in this definition. Yet it suffices for our theoretical purposes. In fact, the specifi­ cation of an actual operator to be implemented in a learning system should consider also other information (such as exam­ ples, background knowledge, etc.), to define the underlying heuristic component.

With respect to maximal specializations, the major diffi­ culty comes from the fact that under standard implication, C U D is a clause that preserves the models of either clause, hence turning out to be a maximal specialization. In this set­ ting, as expected, more clauses are needed than a single one; indeed the following operator has been defined:

Definition 3.6 Let C1 and C2 be two clauses such that C1 and C2 are standardized apart and K a set of new constants such that: IKI ~ I vars( C1 U C2) I· A new set of clauses is defined l,b1(C1,C2) = {CI C = (C1a1 U C2a2)a1 1 a2 1 } where a 1 and a 2 are Sko/em substitutions for, respectively, C1 and C2 with K as their term set 1 ·

Example 3.1 Given two clauses C1 = {p(X, Y), q(X)} and C2 = {p(X', Y'), r(X')}, the Of-substitutions a1 = {Xja , Y/b} and a 2 = {X' ja, Y' /b} yield the following clause: F1 = {p(X, Y) , q(X), r(X)}. Similarly 0'3 = {Xja, Y/b} and a4 ={X' /b, Y' /a} yield the clause: F2 = {p(X, Y), p(Y, X), q(X), r(X)} and so on.

It is easy to see that, clauses (C1a1 U C2a2)a! 1 a2' 1 are equivalent to those in (C1a1 U C2a2)a2 1 a! 1 . Besides, the clauses in 'l,b1(C, D) preserve the OI-models of C and D:

1 The term set of a set of clauses T by the Skolem substitution CJ is the set of all terms occurring in TCJ .

Proposition 3.2 Let C, D and E be clauses such that C and Dare standardized apart. IfCf=o1E and Df=o1E then 1::/F E 'l,b1(C, D): Ff=o1E.

This result implies that [,61 ( C, D) contains maximal special­ izations of the two clauses w.r.t. 01-implication. For the proof of ideality given in the next section, it is important to point out that this set of specializations is finite. Moreover, the defini­ tion of [,61 and also Proposition 3.2 can be extended to the case of multiple clauses [Fanizzi and Ferilli, 2002] .

4 Ideal Operators for Theories

Nonexistence conditions for ideal refinement operators for generic spaces are given in [Nienhuys-Cheng and de Wolf, 1997]. A close relationship has been recognized between ide­ ality and the covers of elements in (S, ::5), a downward cover of C being a D such that D -< C and !3JE : D -< E -< C (resp. C -< D and fJE: C -< E -< D for the upward case). A necessary condition for the ideality of refinement operators is that they return supersets of the sets of covers.

Theorem 4.1 In the quasi-ordered space 2 ( C, ::::o) an ideal refinement operator does not exist.

The non-existence of ideal refinement operators for spaces of clauses ordered by implication can be proven as a conse­ quence of this result [Nienhuys-Cheng and de Wolf, 1997], since B-subsumption is weaker than logical implication. Be­ sides, this can be extended, proving the non-existence of refinement operators for search spaces of theories endowed with the ordering relationship induced by B-subsumption [Midelfart, 1999] and the one induced by logical implication [Nienhuys-Cheng and de Wolf, 1997] . Conversely, within the framework we present, it is possible to exploit the definition of the refinement operators for clausal spaces for demonstrat­ ing the existence of ideal operators on spaces of theories.

4.1 Ideal Operators for 11o1-subsumption

With respect to the spaces of clauses in the generalization model induced by Cbi-subsumption, we exploit the ideality of the operators for clausal spaces [Esposito et a/., 2001 a] .

Definition 4.1 In the quasi-ordered space (2c , ~OJ) , given a theory T, let Tnr be a non redundant theory equivalent to T The downward refinement operator fbi is defined as follows:

• [(Tnr \ S) U {DE fbi( C) ICES}] E fbi(T) where S ~ Tnr
• Tnr \ {C} E fbi(T) with C E Tnr

The upward refinement operator ~1 is defined as follows:

• [(Tnr \ S) U {DE ~I(C) ICES}] E ~~(T) where S ~ Tnr
• Tnr U {C} E ~~(T) with C tj. Tnr

The ideality of these operators is proven as follows:

Theorem 4.2 In the search space (2c, ~OJ), the refinement operators fbi and ~I are ideal. Proof:

2 here ::::o denotes the order induced by e-subsumption and the language is supposed to contain at least a binary predicate.

• fbi: (locally finite) obvious. (proper) by the properness of fbdor clauses. (complete) Suppose T"2:IJ1T' and T' /::n1T. Let T' = { Di I i = 1, .. . , n }. The theories can be supposed to be non redundant, otherwise the reduced equivalent theory can be computed by removing clauses by means of the second item of the operator. By definition T "2:IJ1T' means that \:/Di E T', i E {l , . . . ,n},3Ci ET: Ci?:.OIDi . By the completeness of the operator fb1 for clauses, it holds that Vi E {1, ... , n }3ki: Di E P~l (Ci). Starting from T1 = T, the first component of the op­ erator is iterated, obtaining for each Tj a refinement TJ+1, by choosing Sj as the subset ofTj made up of the clauses that are not in the target theory T' while being strictly more general than clauses in T', that is S j = {C E Tj \ T' I 3D E T': C>0 ,D}. Eventually it holds that 3Tk E p~1 (T) for some k :::; maxf=1 (ki) such that Vi Di E Tk . Tk may be larger than T'. Thus the second component of .lb1 for theories can be employed for deleting the ex­ ceeding clauses from Tk yielding T'. Finally we have that T' E p~1 (T) .

cb1 : Analogously.

4.2 Ideal Operators for 01-implication

These operators above will be embedded in the definition of the refinement operators for spaces of theories in the stronger order induced by OI-implication. Besides, notions and re­ sults given in Section 3.2 are also exploited. In particular, these operators should be able to compute specializations and generalizations that are able to reach those clauses involved in or-resolution steps (and their inverse).

Definition 4.2 In the quasi-ordered space (2c, f=o,), the downward refinement operator fb1 is defined as follows, given anyT E 2c

• l,6,(C)cEsC E fb,(T) where S ~ T
• UcEs((T \ S) u lb/(C)) E fb,(T) where S ~ T and {b/ denotes the downward refinement operator for clauses wrt f=o,
• T' E /b1 (T) ifT' E {b/ 1 (T) where fbi" denotes the downward refinement operator for theories wrt "2:IJ1

The upward refinement operator <b1 is defined as follows:

• T U { C} E cb1(T) where 3R ~ T and C E V01 (T)
• UcE8 ((T \ S) U cb/(C)) E <b,(T) where S ~ T and <b/ denotes the upward refinement operator for clauses wrt f=o,
• T' E <bt(T) ifT' E <b,(T) where <bt denotes the upward refinement operator for theories wrt 2n1

The ideality of these operators is stated by the following result (Figure I depicts the related refinement graph):

Theorem 4.3 In the search space (2c, f=o1) , the refinement operators fb1 and cb1 are ideal. Proof:

fb1 : (locally finite) by definition of the various operators and the finiteness of the theories.

(proper) by the properness of the refinement operators employed in the various items.

(complete) Suppose Tf=o,T' and T' jp01T with n = IT'I. Since redundancy can be eliminated by remov­ ing redundant clauses (and tautologies) through the last item of the operator, we will consider the theories as non redundant. Let us observe that Tf=o,T' is equivalent to \:/Ci E T' : Tf=o,Ci,for i = 1, . .. , n. By Theorem 2./,for each Ci, there exists a Di such that Di E R~! (T), for some ki , and Di ~,-subsumes Ci. Observe that, by using the first item of the refinement op­ erator, it is possible to produce the theory Ts containing the maximal specializations of the clauses in S ~ T employed in the Of-derivation the of Di 's (by the ex­ tension of Lemma 3.2 to the case of multiple clauses where each maximal specialization is more general wrt Of-implication than an Of-resolvent Di): Ts E fb1(T) . Observe that \:IF E Ts Ff=o,Di. Now, it is possible to iterate (at most n times for the Di that are properly by some F) the second item of the operator, in order to computethetheoryTR = {Di I i = l, ... ,n}, thus we can write: TR E p~1 (Ts), k:::; n. By construction Vi Di"2:IJ,Ci, then TR"2:IJ1T 1 , then we can exploit the ideal operator for theories wrt ~1 - subsumption (third item of the operator for theories wrt Of-implication) writing: T' E p~1 (TR)·

Finally, by chaining these steps, it is possible to con­ clude that: T' E p~1 (T) .

• cb1 : In the same hypotheses the previous proof, it is possi­ ble to invert the ~1 -subsumption of TR wrt T' using the last item of the definition of <b1 for theories wrt Of­ implication: TR E o~1 (T') . Then, a number of Of-resolutions are to be inverted by using the first item of cb1· This number is finite due to Proposition 2.3 and then can be done tentatively in afi-

Finally, by chaining these steps, it is possible to con­

nile number of steps. Then T E c5~1 (TR). clude that: T E c5~1 (T').

Differently from the standard generalization models, in this framework the number of OI-resolution steps is bounded be­ cause, during OI-implication or t':l:ll-subsumption steps, the sizes of the clauses increase (decrease) monotonically, as a consequence of Propositions 2.2 and 2.3.

5 Conclusions

In this work the existence of ideal refinement operators was proved in the search space of theories ordered by general­ ization models based on object identity. Coupled with some heuristics, this allows for the definition of efficient refinement algorithms that avoid the myopia of the traditional relational learning approaches.

We focussed on the effectiveness of the refinement opera­ tors, that is related to their static properties. In general this is not sufficient for defining a learning algorithm: efficiency plays a key role when dealing with first order logics. The suc­ cessive step is to investigate the dynamic properties of these operators when they are to be guided by means of heuristics based on the available examples and/or other criteria.

We have also mentioned that in spaces with rare solutions it is more suitable to have an operator that is non redundant, be­ cause almost all of the paths that could be constructed would not lead to a target theory. It should be investigated how to define non redundant operators in this framework.

The object identity framework is currently implemented in the system INTHELEX [Esposito eta/., 2000], with a totally incremental strategy based on clause-level induction. We plan to investigate how to upgrade the system to theory-level, ex­ ploiting the theoretical operators presented in this paper to­ gether with suitable evaluation functions to mitigate the com­ binatorial complexity of the problem.