Proof of soundness and completeness

We provide here a brief introduction and proof of soundness and completeness of the ILP system ASPAL. This document is in support of our ICLP 2011 submission, for the reviewers’ benefits. Inductive Logic Programming (ILP) [4] is a machine learning technique concerned with the induction of logic theories, called target theories, that generalise (positive and negative) examples with respect to a prior background knowledge. For example, from the observations fly(a), f ly(b),¬fly(c) and a background knowledge containing the two facts bird(a) and bird(b), we can generalise the concept fly(X) ← bird(X). In non-trivial problems it is crucial to define the space of possible solutions accurately. Target theories are within a space defined by a language bias, which can be expressed using mode declarations [4]. We refer to [3] for notations and preliminary definitions on logic programming. For a given theory T we denote with BT the Herbrand base of T . Definition 1. A mode declaration is either a head declaration, written modeh(s), or a body declaration, written modeb(s), where s is a schema. A schema is a ground literal containing special terms called placemarkers. A placemarker is either ‘+type’, ‘−type’ or ‘#type’ where type denotes the type of the placemarker and the three symbols ‘+’, ‘−’ and ‘#’ indicate that the placemarker is an input, an output, a constant placemarker, respectively. In the previous example a possible language bias would be given by the three mode declarations modeh(fly(+animal)), modeb(bird(+animal)) and modeb(fish(+animal)). A rule h ← b1, ..., bn is compatible with a set M of mode declarations iff (a) h is the schema of a head declaration in M and bi are the schemas of body declarations in M where every input and output placemarkers are replaced by variables and constant placemarkers are replaced by constants; (b) every input variable in any atom bi is either an input variable in h or an output variable in some bj , j < i; and (c) all variables and constants are of the corresponding type. From a user perspective, mode declarations establish how rules in the final hypotheses are structured, defining literals that can be used in the head and in the body of a well-formed hypothesis. s(M) is the set of all the rules compatible 2 Domenico Corapi, Alessandra Russo with M . For a set M of mode declarations we denote with Mb the subset of body declaration and with Mh the subset of head declaration. Definition 2. An ILP task is a tuple 〈P,B,M〉 where P is a set of conjunctions of literals, called properties, B is a normal program, called background theory, and M is a set of mode declarations. A theory H, called hypothesis, is an inductive solution for the task 〈P,B,M〉, if (a) H ⊆ s(M), and (b) P is true in all the stable models of B ∪H. The above notion is an instance of the learning from entailment setting [2], where positive and negative examples are our properties. In the following we omit the additional control on the type of the arguments in the mode declarations for simplicity and readability. The extension of the definitions and proofs with type check is straightforward, they can be added to the bodies of the hypotheses and of the rules of the additional theories introduced using a standard pre-processing procedure used in ASP. Furthermore, our definitions and proposition will be given for ground programs. Rules with variables will be used as a shorthand for the set of their ground instances. We define a strong completeness requirement, compared to alternative formulations where completeness only requires that a solution is found if one exists. Given a mode declaration id : modeh(s) (or modeb(s)), id is the (unique) identifier for the mode declaration and sc(id) denotes the schema s of the mode declaration. Definition 3. s is the literal obtained from s by replacing all placemarkers with different variables var(s, s) = (X1, ..., Xn), called a variable list and it is called the variabilisation of s. con(s, s) = (C1, ..., Cc) is the constant list of variables in s that replace only constant placemarkers in s. inp(s, s) = (I1, ..., Ii) and out(s, s) = (O1, ..., Oo) are defined similarly for input and output placemarkers. A variable is in the variable list if and only if is one of the constant, input or output list. When s is clear from the context we omit the second argument from var(s, s), con(s, s), inp(s, s) and out(s, s). Given a set of mode declarations M , a top theory > = t(M) is constructed as follows: – For each head declaration modeh(s), with unique identifier id, the following rule is in > s← rule(RId, (id, con(s), ()), rule id(RId), body(RId, 1, inp(s)) (1) – For each body declaration modeb(s), with unique identifier id the following clause is in > body(RId, L, I)← rule(RId, L, (id, con(s), Links)), link(inp(s), I, Link), s, append(I, out(s), O), body(RId, L + 1, O) (2) ASPAL. Proof of soundness and completeness. 3 – The following rules are in > together with a standard definition for the append predicate. body(RId, L, )← rule(RId, L, last) (3) link((X), (X), 1). link((X), (X, ), 2). link((X), ( , X), 2). link((X,Y ), (X,Y ), (1, 2)). link((X,Y ), (Y,X), (2, 1)). link((X), (X, , ), 1). link((X), ( , X, ), 2). ... (4) rule id(1). ... rule id(rn). (5) rule id(rid) is true whenever 1≤ rid≤ rn where rn is the maximum number of new rules allowed. link((a1, ..., am), (b1, ..., bn), (o1, ..., om)) are true if for each element in the first list ai, there exists an element in the second list bj such that ai unifies with bj and oi = j. Given the top theory, we seek a set of rule atoms ∆, such that P is true in all models of B ∪ > ∪∆. ∆ has a one-to-one mapping to a set of rules H = u(∆,M). Intuitively, each abduced atom represents a literal of the rule identified by the first argument. The second argument collects the constant used in the literal and the third defines the variable linking. ∆rid denotes the subset of ∆ of all the rule abducibles with rid as a first argument. Each ∆rid corresponds to a rule r in u(∆,M), r = u(∆rid,M). For a given ∆rid ={rule(rid, (idh, conh), rule(rid, 1, (id1, con1, links1)), ..., rule(rid, 1, (idn, conn, linksn))} r is a rule h← b1, ..., bn such that, given a list of variables defined as follows: – avar0 is inp(sc(idh)) – avari is such that append(avari−1, out(sc(idi)), avari) is true for each i = 1, ..., n for the standard definition of append each atom is constructed as follows: – h = sc(idh) and con(sc(idh)) is unified with the list of constant conh of the same length 4 Domenico Corapi, Alessandra Russo – bi = sc(idi), con(sc(idi)) is unified with the list of constant coni of the same length and link(inp(sc(idi)), avari−1, linksi) is true, according to the definition of link provided in the top theory for each i = 1, ..., n Proposition 1. Let H be a theory and M a set of mode declarations. Then H ∈ s(M) if and only if there exists a ∆ such that H = u(∆,M). Proof. The proof is immediate as the transformation itself can be used to define s(M). In fact the transformation requires that the head corresponds to the variabilisation of a schema of a head declaration where all the constants are replaced by arbitrary constants. Each other condition i in the body can only bind input to variables in avari−1 by definition and the constants are also replaced by a list of arbitrary constants. u t In the proof we will use the unfolding transformation or generalised principle of partial evaluation (GPPE)[1]. Definition 4. Let P be a theory, h ← b1, ..., bi−1, bi, bi+1, ..., bn ∈ P a rule r and bi a positive literal. We say we apply a GPPE transformation to r on bi if P ′ is the theory obtained from P by replacing rule r with the p rules h← b1, ..., bi−1, bi+1, ..., Aj where Aj is the conjunction of literals in bi ← Aj ∈ P , j = 1..p. Definition 5. Let P and Q be theories. We say P is equivalent to Q if, for all interpretation I, I is a stable model for P if and only if I is a stable model for Q. Proposition 2. [1] Let P be a theory. If P ′ is the theory obtained applying GPPE to any rule in P then P ′ and P are equivalent. Proposition 3. Let B be a normal program, H be a hypothesis and M a set of mode declarations such that H = u(∆,M) and > = t(M). Let α denote B ∪H and β denote B ∪ > ∪ ∆. Let K = I ∪ J be an interpretation for β such that I ⊆ Bα, J ⊆ (Bβ \ Bα). Then K is a stable model for β if and only if I is a stable model for α. Proof. Consider rules (1) of the top theory. Applying GPPE to them on body(RId, 1, inp(s)) we obtain a theory >1 in which rules (1) are replaced by the following: sc(idh)← rule(RId, (idh, con(sc(idh)), ()), rule id(RId), rule(RId, 1, (id1, con(sc(id1)), Links1)), link(inp(sc(id1)), inp(sc(idh)), Links1), sc(id1), append(inp(sc(idh)), out(sc(id1)), O1), body(RId, 2, O1) (6) ASPAL. Proof of soundness and completeness. 5 for all idh such that idh ∈ Mh and for all id1 ∈ Mb. We used the rules (2) where the second argument is 1. Using (3) in the transformation the following rules are included in >1 sc(idh)← rule(RId, (idh, con(sc(idh)), ()), rule id(RId), rule(RId, 1, last) (7) We can now apply the transformation again on body(RId, 2, O1)) and rules (2) and (3), and again on body(RId, i+ 1, Oi) for each i ≤ nc. nc the maximum number of conditions allowed is enforced by an additional condition on the second argument of the body predicate, omitted for ease of exposition. So we obtain a theory >′ that contains the following rules for each m = 1..nc. sc(idh)← rule(RId, (idh, con(sc(idh)), ()), rule id(RId), rule(RId, 1, (id1, con(sc(id1)), Links1)), link(inp(sc(id1)), inp(sc(idh)), Links1), sc(id1), append(inp(sc(idh)), out(sc(id1)), O1), ..., rule(RId, n, (idm, con(sc(idm)), Linksm)), link(Om−1, inp(sc(idm)), Linksm), sc(idm), append(Om−1, out(sc(idm)), Om), rule(RId,m+ 1, last), (8) and for all id such that id ∈Mh and idi ∈Mb, i = 1, ..,m. Of these rules the only rules whose body can be true are those that contain exactly the atoms in ∆rid for some rid. C