A Theory of Clausal Discovery

1 Introduction

A framework for discovering general first order clausal theories (sets of clauses of the form Pl 1\ ... 1\ PI< -+ q1 V ... V qm, where the Pi and q; are first order atoms) from databases is presented. It is incorporated in the system CLAUDIEN (CLAUsal Discovery ENgine). CLAUD lEN combines ideas from the area of knowledge discovery (KDD), inductive logic programming (ILP) and deductive databases. From knowledge discovery in databases [Piatetsky-Shapiro and Frawley, 1991], CLAU­ DIEN inherits its aim: finding regularities from (poten­ tially large) databases. However, in contrast to most of the current work in knowledge discovery, CLAU­ DIEN employs a first order logic framework. Current work in knowledge discovery has mainly used proposi­ tional and/or attribute-value representations, or has fo­ cussed on learning specific forms of first order sentences, such as for instance: determinations [Shen, 1992], and u.mctional and inclusion dependencies [Kantola et al., 1992, Flach, 1990]. CLAUDIEN shares its motivation for employing a first order logic framework with induc­ tive logic pro~ramming [Muggleton, 1992, De Raedt and Lavrac, 1993]: logic facilitates the use of background knowledge and is much more expressive than proposi­ tional or attribute-value representations. Furthermore, there is a strong relation between lo&ic programming and deductive databases [Minker, 1987], which provides a solid theoretical basis for clausal discovery. Since clausal theories are often used as integrity theories in deductive databases, CLAUDIEN can be applied to automatically derive integrity theories/constraints from databases. Clausal theories are easy to understand. Therefore CLAUDIEN also contributes to the induc­ tive engineering and knowledge synthesis paradigms pro­ posed by Donald Michie and Ivan Bratko [Bratko, 1992].

·The authors are supported by the Belgian National Fund for Scientific Research and the ESPRIT III contract no. 6020 on Inductive Logic Programming.

CLAUDIEN employs an efficient iterative deepen­ ing search strategy, where clauses are expanded using a clausal refinement operator, and where pruning is achieved by checking whether a candidate clause is im­ plied by the current clausal theory or not, and whether a clause contains redundant information or not. CLAU­ DIEN derives a minimally complete theory satisfying a given database. Roughly speaking, this means that the theory derived is most informative (i.e. logically maxi­ mally general) and logically non-redundant (i.e. deleting clauses from the theory results in loosing information).

In Section 2, we present the theoretical framework of CLAUDIEN; in Section 3, the basic algorithm of CLAU­ DIEN is specified and illustrated; in Section 4, we report on some experiments with CLAUDIEN; and in Section 5, we conclude, review related work and indicate some directions for future work.

2 Problem specification

We briefly review some notions of logic programming (see [Lloyd, 1987] for more details):

Definition 1 A databa6e D u a 6et of normal program clau6e6.

Definition 2 A normal program claU6e u a logical ez­ preuion of the form p +- lt 1\ ... 1\ ln, where p u a po6itive atom and the li are po6itive or negative atom8.

Definition 3 A clau6e c u a logical ezpreuion of the form p1 1\ ... 1\ PI< -+ q1 V ... V qm where the Pi and q; are po6itive atom6. body( c) denote6 P11\ ... I\ PI< and head( c) denote6 q1 V ... V qm.

Sometimes, we will use the equivalent disjunctive not~ tion of clauses, i.e. 'Pl V ... V 'Pio V q1 V ·.. V qm. As lD most work on deductive database we assume that clauses are range-restricted:

Definition 4 A clau6e c i6 range-redricted if and only if all variable6 occurring in head( c) al6o occur in body( c).

There are many different semantics for normal programs. While they all agree for certain classes of programs, there can be subtle differences for programs involving recur­ sion. Here, we adopt the completion semantics and the SLDNF proof procedure. Nevertheless, for function free databases one could argue in favor of a semantics select­ ing a particular model, such as the well-founded seman­ tics for general logic programs [Van Gelder et al., 1991], and a sound and complete proof procedure such as [Chen and Warren, 1992]. In what follows, completion seman­ tics and SLDNF are replaceable by such a semantics and ita corresponding proof procedure.

Definition 5 A clatue c ·atufie· a databa.e D if and onlr if Comp(D) ~ c. A clatue c violate· a databa.e D if and only if Comp(D) ~-.c.

Comp(D) denotes the completion of the database as pro­ posed by Clark 1 . A clause that neither satisfies nor vi­ olates the database is consistent, i.e. it is true in certain models and false in other models of the completion. The following result follows from the soundness of SLDNF resolution.

Lemma 1 If the query .- body( c) 1\ -.head( c) ·ucceed· under SLDNF with ·ub.titution 9 (i.e. Comp(D) rsLDNF body(c) 1\ --.head(c)9) then c violate· D,· if the query finitely fail· under SLDNF then c ·atufie· D.

The result provides us with an incomplete method to verify whether a clause c satisfies a database or not. To check whether a clause c violates or satisfies a database we apply SLDNF-resolution (rsLDNF, cf. [Lloyd, 1987]) (i.e. the PROLOG execution mechanism) on the query. If the query succeeds, the clause violates the database. If the query finitely fails, the clause satisfies the database. Otherwise, the result is undefined: the query does not terminate.

Notice also that our semantics for ILP differs from the usual B 1\ H ~ E+ and B 1\ H ~ E- semantics in ILP [Muggleton, 1992]; see [De Raedt and Lavrac, 1993, Helft, 1989] for a detailed discussion. The differ­ ences are related to the closed world assumption. In the usual ILP setting, the intended model is only partly specified by means of an incomplete set of positive and negative examples. In our framework, only the true facts (positive examples) are specified, and all facts not spec­ ified are considered false (by the completion and the closed world assumption). Therefore the intended model is much more constrained in our approach than usu­ ally. As a consequence fewer clauses will be acceptable in our semantics and there are no problems with de­ pendencies when learning multiple predicates [De Raedt and Lavrae, 1993]. To illustrate this, assume D = {flies(tweety), bird(tweety), bird(oliver)}. In the classical setting, bird(B) .- flies(B) is acceptable as flies(oliver) is unknown, whereas in our approach this clause violates D as flies(oliver) is assumed to be false. Only if a com­ plete example set is specified will clauses induced in the classical ILP setting also be solutions in our framework.

1 Throughout the paper we will assume that Comp(D) is always logically consistent.

As in inductive machine learning, CLAUDIEN em­ ploys a declarative user-specified bias: the user has to specify the desired form that clauses discovered by CLAUDIEN should take. To make abstraction of the particular bias employed, we will employ the notion of a language C of clauses. For ease of presentation, we will consider C as a set of clauses. A partial order on clauses is induced on C by Plotkin's notion of 9-subsumption:

Definition 6 Clatue c 8-1ub·ume· clatue c' if and only if there u a ·ubltitution 9 ·uch that c9 C c' and there u no 111.b.titution u ·uch that c' u C c.

The problem addressed by CLA UDIEN, is that of dis­ covering a minimally complete theory that satisfies a given database and language C.

Definition 7 A theory u a ·et of range-reltricted clatuel.

Definition 8 A theory T C C u complete for a language C and a databa.e D if and onlr if Comp(D) ~ T and VT' C C: (Comp(D) ~ T')--+ T ~ T'.

A theory is thus complete for a language if it is a max­ imally general subset of the language that satisfies the database (we employ the usual notion of logical general­ i·ation here).

Lemma 2 For a given databa1e D and language C, all complete theorie1 are logically equivalent.

Proofs of lemma's and theorems are contained in [De Raedt and Bruynooghe, 1993]. Complete theories capture all knowledge in the database that is expressible within the given language. Since all complete theories are logically equivalent, the most interesting ones are the minimal ones. Minimality requires that no clause in T is logically redundant.

Definition 9 A theory T u minimal with re·pect to a databa1e D if and only if --.3c E T: T- {c} ~c.

Theory T is minimally complete with respect to database D and language C.

3 A clausal discovery algorithm

3.1 Refinement

The key to the clausal discovery algorithm is Lemma 1. It states that when a clause c violates a database D we must have that Comp(D) ~ body(c)9 and Comp(D) ~ --.head(c)9 for a certain substitution 9. Since we assume the database to be correct, there are two ways of modi­ fying the clause to make it satisfy the database~:

2 The situation here is essentially dual to that considered by [De Raedt and Bruynooghe, 1992], where clauses are. as­ sumed correct and the database is modified.

• condition body(c) can be strengthened so that body(c) is true for less substitutions 8;
• conclusion head(c) can be weakened so that head(c) is false for less substitutions 8.

Both operations can be achieved using a refinement op­ erator based on Plotkin's 8-subsumption.

Definition 10 A refinement operator p (with tran1itive clo&ure p*) for a language £ i6 a mapping from £ to 2.c &uch that

1. '1:/c E £: p(c) C {c 1 E £ I c 1 i6 a mazimal &peciali&a­ tion of c under 8-&ub&umption}, and
2. p i6 complete, i.e. p* (T) = £ where T i1 the mo&t general element in £.

Completeness means that all elements of the language can be generated using p. In our framework, optimal refinement operators are the most desirable ones :

Definition 11 A refinement operator p (with tran1itive clo&ure p·} i6 optimal if and only if '1:/c, c1, c2 E £ : c E p*(c1) and c E p*(c2)-+ c1 E p*(c2) or c2 E p*(cl)·

Optimal refinement operators are more efficient than classical refinement operators because they generate each candidate clause exactly once. A known problem with classical refinement operators is that they gener­ ate candidate clauses (and their refinements) more than once, making the search intractable. Optimality is thus desirable for efficiency reasons.

3.2 Pruning

Our clausal discovery algorithm employs a complete top­ down search of the refinement graph. In this section, we present two lemma's that allow to prune a clause (and its refinements), without loss of completeness.

Lemma 3 For any refinement operator p, and clau1e1 c, c 1 &uch that c 1 E p*(c) : c ~ c 1 ·

Clauses already implied by the current theory may be pruned without losing completeness. The lemma states that also the refinements of such clauses will be implied by the theory. Therefore, when a clause is implied, the clause together with all its refinements may be pruned.

When the considered language is fair, the search can also be pruned by Lemma 4.

Definition 12 A language £ i1 fair if and only if '1:/ c1, c2, ca E £ and &ubltitution& 81, 82, c1 lh C c2 and c282 C ca-+ c18182 U (ca- c282) E £.

Suppose c1 = A, c2 = A81 U B, ca = A8182 U B82 U C, where A, B, C represent disjunctions of literals (i.e. clauses). For an illustration of fairness and its use, see the example below Lemma 4.

Lemma 4 Given a databa1e D, a fair language £, and 'l:/c1 E £,c2 E p*(c1),c181 C c2 : Comp(D) ~ (c2c181) -+ c181, then c2 and it1 refinement& may be pruned without lo&ing completeneu.

The lemma states that refinements c2 = c181 U d of c1 contain redundant information if d implies c181 with regard to Comp(D). Given a fair language £ we may prune c2 as well as its refinements. To illustrate the lemma, reconsider Example 1 and assume c1 = -. male(X) and c2 = -. male(Y) V -. human(Y). c2 - c181 implies c181, i.e. -. human(Y) implies -. male(Y) in Comp(D), therefore c2 contains redundant information (human(Y)), and may be pruned. Fairness requires that if clause ca = -. male(Z) V -. human(Z) V -, taii(Z) E £, also clause c4 = -. male(Z) V -. taii(Z) E £. If the considered language is fair, pruning c1 is allowed as c4, which is equivalent to c3 with regard to Comp(D) but 8-subsumes ca, will be considered.

3.3 A clausal discovery algorithm

T := 0 Q := {T} while Q ::/; 0 do delete c = (h +-- b) from Q if+-- b 1\ -.h finitely fails using SLDNF on D 1> 0 <l then if T If c 1> 1 <l then add c to T else for all c' E p(c) where c' = c8 U d do if +-- d 1\ -.c8 does not finitely fail under SLDNF on D 1> 2 <l then add c' to Q for all clauses c in T do select next clause c from T if T - { c} 1- c 1> 3 <l then delete c from T

This algorithm defines CLAUDIEN: it starts from an empty theory T, and a queue Q containing only the most general element in the considered language £. It then applies a search process where each element c is deleted from the queue Q, and tested for satisfaction with regard to the database D. If the clause satisfies the database, and is not yet implied by the current theory, it is added to the theory. If the clause does not satisfy the database, its refinements are considered. Because of Lemma 4, some refinements can be pruned if the lan­ guage£ is fair . If the language is not fair, the condition at 1> 2 <l should be removed. Let us therefore refer to the algorithm, including the condition at point I> 2 <l as CLAUDIEN.FAIR, and to the algorithm without this condition as CLAUDIEN.SIMPLE. When the search process terminates, redundant clauses are removed from the theory. This is needed for finding a minimal the­ ory. Indeed, CLAUDIEN may find clauses c1 and c2 in the specified order, and it may be that c1 ~ c2 but c2 ~ c1. The select function in the for-loop has to se­ lect the clauses in the reverse order they were learned (LIFO-strategy).

Notice that the algorithm does not specify the search strategy. To discover clausal theories, one can use essen­ tially any search-strategy, which includes : depth-first, breadth-first, beam-search, best-first, iterative deepen­ ing, etc. Our current experiments (see Section 4) show that depth-first iterative deepening performs very well.

Throughout this paper, we will assume that Algorithm 1 always terminates, an assumption which does not hold in general. Indeed, CLAUDIEN may not terminate be­ cause of two reasons: the refinement graph may be infi­ nite (which may lead to infinite paths through the search apace), or the tests whether T 1- c and/or tests involv­ ing SLDNF may not terminate. Using a bound on the depth of the tree, SLDNF can be forced to terminate. If SLDNF does neither succeed nor fail within the bounds, we assume there is no finite failure. For DATALOG, fi­ nite languages and a well-founded semantics, a variant of this algorithm can be designed that always terminates.

3.4 A detailed example with CLAUDIEN

Suppose we start CLAUDIEN from the database D and language C specified in Example 1. Notice that Cis fair. A simple optimal refinement operator u can be defined as follows:

1. u(T) = { ·l ll E B+} where B+ = {female(X), male(X), human(X)}
2. u(h V ·.. V l,.) = {h V ... V l,. V l,.+l I l,.+l E B and for all i : Z. f l,.+l, ·l· f l,.+l and l, comes alphabetically before 1,.+1},

where B:B+ u{ -,female(X), -.male(X), ·human(X)} Employing breadth-first results in the following steps (the indices indicate the number of previous steps through the while-loop):

To = 0; Qo = {T}; . T1 = 0; Q1 = u(T) = {cl,cl,ca} T2 = 0; Q2 = {c2, ca, cs, C& } T3 = 0; Q3 = {ca, cs, C&, cs, cg, c10, cu} T4 = 0; Q4 = { cs, C&, cs, cg, c1o, cu, c1a} Ts = {cs}i Qs = {c&,cs,cg,clO,cu,cla} T& = {cs,c&}i Q& = {cs,cg,clo,cu,cla} T1= {cs,c&}iQ7= {cg,clo,cll,cla,cl4} Ts = {cs, c&}i Qs = {c1o, cu, c13, c14} Tg = {cs, c&}; Qg = {en, c131 c14, c17} T1o = { cs, c&}i Q10 = { c1a, cu, c11} Tu = {cs,c&,cla};Qu = {c14,c17} T12 = {cs, C&, c1a}; Q12 = {c11} T1a = {cs, C&, c13, c11}; Q13 = 0 u(T) {c1=female(X) -+ c2=human(X) -+ ; c3=male(X) -+ } u(ct)={ c4=female(X) A humah(X) -+ (pruned 1> 2 <] ); c5=female(X) A male(X)-+ ; c6=female(X) -+ human(X); c7=female(X) -+ male( X) (pruned 1> 2 <])} u(c2) ={cs=human(X)A female(X)-+ ; c9=human(X) A male(X)-+; c1o=human(X)-+ female(X); c11=human(X) -+ male(X)} u(ca)={c12=male(X) -+ female(X) (pruned 1> 2 <l); c13=male(X) -+ human(X)} u(cs)={c14 = human(X) A female(X) A male(X) -+ (pruned 1> 1 <] ); c15 =human(X) A female(X)-+ male(X) (pruned 1> 2 <l )} u(c9)={c16=human(X) A male(X)-+ female(X) (pruned t>2<J)} u(c1o)={c11=human(X) -+ female(X) V male(X)} u(cu) = 0

3.5 Properties of CLAUDIEN

In this section, we show that CLAUDIEN, when it termi­ nates and SLDNF proofs always terminate with success or finite failure, discovers minimally complete theories satisfying a given database.

Theorem 1 Given a databtUe D 1 a language C 1 and a refinement operator p for C 1 CLAUDIEN.SIMPLE du­ cover· a minimally complete theory 6atufving D.

Theorem 2 Given a databtUe D 1 a fair language C 1 and a refinement operator p for C 1 CLAUDIEN.FAIR ducov­ er· a minimally complete theory ·atufving D.

4 Practical aspects

In this section, we discuss the implementation of CLAU­ DIEN, its intended use and applications, as well as some experiments.

4.1 Implementation of CLAUDIEN

A prototype of Algorithm 1, named CLAUDIEN, has been implemented in Prolog by BIM. It uses depth-first iterative deepening (cf. [Korf, 1985}) together with a clever indexing scheme. Depth-first iterative deepening is the right strategy for CLAUDIEN, because

• It has essentially the same behaviour as breadth­ first, which makes that simple constraints are dis­ covered before more complex ones.
• It has the memory-efficiency of depth-first search but cannot get lost in infinite paths .
• To avoid the expensive (re)computation of the tests at points 1> 0,1,2 <], we store the result of these tests using a clever indexing scheme (for each clause c we encode the result of the tests in an integer; in the next iterations the clauses c are recomputed but the corresponding tests are not re-evaluated as the result can be looked up in a table). This re­ quires some additional memory, but saves a lot of (re)computation as all tests are done only once. 3

We currently employ an optimal refinement operator for a fair language of range-restricted clauses containing neither functors nor constants. The refinement operator refines a clause by adding one literal at a time.

As T is not a program but a clausal theory, we em­ ploy Mark Stickel's fast theorem prover [Stickel, 1988] to check whether T 1- c at points 1> 1,3 <]. This works very well in practice. Tests involving SLDNF resolu­ tion are currently realized using depth bounded SLDNF­ resolution.

4.2 User involvement

When applying CLAUDIEN on a database containing a large number of predicates, CLAUDIEN has to search a vast search space. This is impractical for all but the sim­ plest databases. Therefore, we believe that it is crucial that the user supplies additional constraints to CLAU­ DIEN. In the current implementation, the user has sev­ eral options available:

• The user can ask CLAUDIEN to consider only clauses involving certain predicates in the head, and certain predicates in the body (this corresponds to stating a kind of clausal determination). Such

3 Alternatively, as in FOIL, to save computation, one could use the result of teat t> 0 <1 for Clause c when evaluating t> 0 <1 for a refinement c' E p(c).

knowledge is often available to domain experts, who have certain expectations about the relevant regu­ larities in their domain. These expectations signif­ icantly reduce the search, and can be done incre­ mentally: first look for relations between predicates Pi and then for relations between predicates q;, etc. The user can also specify the maximum number of variables and literals in a clause.

• The user can impose certain criteria on constraints to be acceptable. For instance, to allow for noise handling, the user can relax the condition Comp(D) f-sLDNF c into (pft) > X, where p =I {9 I Comp(D) f-sLDNF body(c)9 1\ head(c)9} I and t =I {9 I Comp(D) f-sLDNF body(c)9} I, where X is a parameter indicating in how much per cent of the substitutions the clause is satisfied. I S I is the cardinality of S. The user can require that clauses c with a non-empty head have a value for t > Y, re­ flecting a principle that clauses matching only few cases, are less reliable.
• The user can restrict the form of clauses such that only definite clauses are considered.

A planned extension of the current implementation, is to provide the user with a refinement operator based on schemata as in the MOBAL - BLIP system [Kietz and Wrobel, 1992]. A schema is a second-order expres­ sion involving predicate variables, such as 3P : P(X,Y) 1\ P(X,Z) --+ Y = Z. The notion of 9 subsumption has been extended towards this second-order expressions by [Kietz and Wrobel, 1992]. Using second-order schemata, CLAUDIEN can derive specific forms of clauses. Given the above expression, CLAUDIEN would derive func­ tional dependencies. In this context, CLAUDIEN can potentially and efficiently simulate some of the work in knowledge discovery in databases that focuses on dis­ covering such specific dependencies ( cf. [Kantola et al., 1992, Flach, 1990]).

4.3 Illustration

We ran CLAUDIEN on a database containing family re­ lations father, mother, parent, male, female and human. The language restricted clauses to contain at most two variables and at most 3 literals. Any combination of predicates in clauses was allowed. CLAUDIEN derived the following theory:

female(V36)1\male(V36)--+ false male(V33)--+ human(V33) (1) female(V33) --+ human(V33) (2) human(V33) --+ female(V33)Vmale(V33) (3) parent(V33,V33) --+ false mother(V33,V34)--+ parent(V33,V34) father(V33, V34) --+ parent(V33, V34) parent(V36, V37)1\parent(V37 ,V36) --+ false father(V36, V37)1\mother(V36, V37) --+ false parent(V33,V34) --+ father(V33, V34 )Vmother(V33,V34) parent(V33,V34)--+ human(V34) parent(V33,V34)--+ human(V33) mother(V33,V34) --+ female(V33) father(V33,V34)--+ male(V33)

The induced theory contains most of the relevant in­ formation about the involved predicates. The theory can be used as an integrity theory for a database about the predicates. The theory also contributes to under­ standing the domain of family relations as the regular­ ities in the theory are easily understandable. Clausal theories are also very powerful for making predictions. Indeed, if parent(luc,soetkin) and male(luc) is known we can derive -. mother(luc,soetkin), father(luc,soetkin), fe­ male(soetkin) V male(soetkin), human(soetkin), etc. On the other hand, if only father(luc,soetkin) is known we can derive human(luc), human(soetkin), female(soetkin) V male(soetkin), male(luc), parent(luc,soetkin), -. fe­ male(luc). It is easy to see that using the above the­ ory, prediction can start from basically any fact(s) for any set of predicates. This contrasts significantly from the usual inductive logic programming setting, where the inferences only go in one direction. Given the usual ap­ proaches, the learner would induce only clauses for spe­ cific predicates. E.g. the clauses (1) and (2) could be inferred, or alternatively the two normal clauses corre­ sponding to clause (3), i.e. male(X) +- human(X) 1\ -. female(X) ( 4) and female(X) +- human(X) 1\ -. male(X) (5). Most of the current inductive logic programming systems would not allow to induce both (1-2) and (45), because the resulting program loops. Because of this restriction, the induced theory can only be used in one direction. Given ( 4-5) one can derive facts for male and female from facts for human, male and female. Given (12), facts for human can be derived from facts for male or female. Using clausal theories, one does not suffer from this restriction.

5 Conclusions and Related Work

CLAUDIEN significantly extends the current work in KDD and ILP:

First, clausal theories are much more expressive than the representations currently being used in KDD and ILP. This has two effects: 1) clausal theories can express regularities that cannot be expressed in the other rep­ resentations (e.g. parent(X,X) --+ cannot be expreBSed using definite clause logic), and 2) clausal theories can represent some regularities in a more compact way (e.g. human(X) --+ female(X) V male(X) could be expressed by two normal program clauses female(X) +- human(X) 1\ -. male(X) and male(X) +- human(X) 1\ . -. female(X)). Property 2) makes clausal induction potentially more ef­ ficient than classical ILP as one full clause corresponds to several normal program clauses. Property 1) does not necessarily imply that clausal induction is computation­ ally more expensive than classical ILP as the approach can be tuned towards specific forms of clauses by using schemata.

Second, the use of a different semantics puts several issues in ILP in a new perspective (see also [De Raedt and Lavrac, 1993]): because the intended model is more constrained than usually, fewer clauses are acceptable in our framework and empirically learning multiple pred­ icates is plausible. Empirically learning multiple pred­ icates is one of the unsolved problems in current ILP.

Indeed, moat ILP systems, such as GOLEM [Muggle­ ton and Feng, 1990] and FOIL [Quinlan, 1990], focus on learning a single predicate and may run into problema when learning multiple predicates ( cf. [De Raedt et al., 1993, De Raedt and Lavrac, 1993]).

Third, we have shown that CLAUDIEN can also be used in deductive databases as an aid to semi-automate the formulation of an integrity theory. In deductive databases, one could start from a small database that is known to be integer. Running CLAUDIEN on such a database can help in formulating the integrity theory.

Finally, there are several remaining issues for future work. To evaluate the applicability of CLAUDIEN, real-life experiments should be performed. Furthermore, heuristics may be needed in such applications to cope with noise and to consider only the moat interesting clauses. We already proposed two heuristics (the per­ centage of covered substitutions and the minimum cover­ age of the body for clauses with a non-empty head), but further experience is needed to find out whether these are satisfactory. Another important issue for applying clausal discovery in practice is to provide the user with tools to declaratively specify bias. Such bias is needed to restrict the search space and to make clausal discovery feasible on large databases containing many predicates and facts. Our work also leaves some open theoretical questions about clausal discovery. For what languages do optimal refinement operators exist? What is the compu­ tational complexity of the discovery algorithm? How to handle non-termination elegantly ?

Acknowledgements

The authors are grateful to Ivan Bratko, Marc Denecker, Peter Flach, Nada Lavrac, Bern Martens, Stephen Mug­ gleton, Gunther Sablon and Marc Van Barel for discus­ sions, suggestions and encouragements.