Tensor-Based Abduction in Horn Propositional Programs

Abstract

This paper proposes an algorithm for computing solutions of abductive Horn propositional tasks using third-order tensors. We rst introduce the notion of explanatory operator, a single-step operation based on inverted implication, and prove that minimal abductive solutions of a given Horn propositional task can be correctly computed using this operator. We then provide a mapping of Horn propositional programs into third-order tensors, which builds upon recent work on matrix representation of Horn programs. We nally show how this mapping can be used to compute the explanatory operator by tensor multiplication.

Keywords

• Abduction
• Linear Algebra
• High-Order Tensor

Introduction

Linear algebra plays a central role in both Arti cial Intelligence and Machine Learning. In particular, statistical approaches to AI often involve analysis and manipulation of feature vector spaces for the purpose of learning and inference. For example, high-order tensors and dense vectors have been employed to support logic-based deductive and inductive inference [ 11,8 ], but for a limited class of logic programs. The area of symbolic AI, however, has seen only limited usage of linear algebra. Two methods have recently been proposed for embedding logic programs into vector spaces. The rst, [ 10 ], allows the computation of the truth value of a First-Order formula using tensor products. The second, [ 9 ], o ers a characterization of logic programs using linear algebra by mapping Horn logic programs into matrices, and disjunctive and normal programs into third-order tensors in order to support deductive inference.

Our work builds upon these recent results as a rst step towards a tensorbased approach for inductive learning. Abduction plays an important part in the inference of knowledge completion, and is related to deduction and Clark Completion [ 1 ]. It has been used in several inductive logic programming approaches. For instance, XHAIL [ 7 ] uses abductive inference to compute suitable head atoms for hypothesis clauses, and both ASPAL [ 2 ] and Metagol [ 6 ] use an abductive meta-representation of the hypothesis space to search for inductive solutions.

An abductive task includes an observation, a background knowledge, in the form of logical rules, and a set of abducible atoms (or explanations), with which to construct an explanation to the given observation. Explanations must be consistent with the given background knowledge and integrity constraints (if any). An abductive solution is a subset of abducibles that, together with the background knowledge, consistently explain the given observation. In this paper we consider abductive tasks where the background knowledge is represented as a set of propositional Horn clauses. We refer to such a task as an abductive propositional Horn task. Drawing on the work of Sakama et al. [ 9 ], we propose an algorithm for computing solutions of an abductive propositional Horn task using third-order tensors. We rst introduce the notion of explanatory operator, a single-step operation based on inverted implication. We prove that minimal abductive solutions of an abductive propositional Horn task can be correctly computed using this operator. We then provide a mapping for expressing sets of propositional Horn clauses into third-order tensors and show how this mapping can be used to compute the explanatory operator by tensor multiplication.

The paper is structured as follows. Section 2 introduces the basic notions and terminologies. Section 3 presents our approach with theoretical results and Section 4 discusses its implementation and future research directions. 2

Background

We assume the reader is familiar with logic programming, linear algebra and the basics of high-order tensors [ 5 ]. A Horn rule is of the form h b1 ^ b2 ^ ::: ^ bn, where h; b1; b2; :::; bn are propositional variables (called atoms) belonging to an alphabet . The atom h is the head of r, denoted head(r), and the set of atoms fb1; b2; :::; bng is the body of r, denoted body(r). Constants ? and > represent false and true respectively and also belong to . A fact is a rule of the form h >, and a constraint is a rule of the form ? b1 ^ ::: ^ bn. A Horn program P is a nite set of Horn rules, facts and constraints. The set of atoms that appear in P , along with ? and >, is called the Herbrand base of P and denoted BP . An Interpretation I of P is a subset of BP , containing also > (implicitly). If I contains ? we say I is inconsistent. I is a model of P if it is consistent and satis es the property: if body(r) I then head(r) 2 I. We say a program P is satis able, denoted sat(P ) if it has a model, and if not we write unsat(P ). Horn programs have at most one minimal model, called the Least Herbrand Model (LHM (P )) [ 12 ]. A program P [ I is a short hand notation for adding the atoms of I as facts to a program P . The Immediate Consequence operator of a program P , TP , is de ned over interpretations by TP (I) = head(r) r 2 P; body(r) I . For every Horn Program P there exists a smallest natural number n such that TPn+1(;) = TPn(;). TPn(;) is called a xed point. If a program is satis able, the xed point is equal to LHM (P ) [ 12 ].

Sakama et al. have proposed in [ 9 ] a mapping of Horn programs into matrices. This is de ned only for programs that satisfy a Multiple De nitions (MD) condition: for every two rules r1 and r2 such that head(r1) = head(r2) then jbody(r1)j 1 and jbody(r2)j 1. In other words, if an atom is head of more than one rule, then those rules must have no more than one propositional variable in their body. It has been shown that every program can be mapped into a program satisfying the MD condition [ 9 ].

We now describe a modi ed version of the mapping proposed in [ 9 ]. Let P be a Horn program with Herbrand base BP = f?; >; p3; :::; pN g. First, elements of BP are mapped into one hot-vectors in RN . An interpretation I can be mapped into a vector vI by setting vi = 1 if pi 2 I, else vi = 0. A program P is mapped into a matrix DP 2 RN N as follows. For every rule r of the form pi pj1 ; pj2 ; :::; pjm , the elements DiPj1 = DiPj2 = ::: = DiPjm = m1 . Elements D1P1 = ::: = DNP1 = 1, indicating that \? implies everything", and elements D2P1 = ::: = D2PN = 1, denoting that \everything implies >". Finally, di erently from [ 9 ], we also set D1P1 = D2P2 = ::: = DNPN = 1, representing the tautologies pi pi for every atom pi in P . This addition is required for the abductive procedure we propose. As an example, for the program P = fp q ^ r; q t; r >; t s; ? sg, the corresponding matrix DP can be seen on the right.

? > p q r t s ?2 1 0 0 0 0 0 1 3 >6 1 1 1 1 1 1 1 7 p66 1 0 1 21 21 0 0 77 q66 1 0 0 1 0 1 0 77 r66 1 1 0 0 1 0 0 77 t 64 1 0 0 0 0 1 1 75 s 1 0 0 0 0 0 1 Let now H1 : R ! f0; 1g be de ned as H1(x) = 1; if x 1, else 0. Analogously to Proposition 3.2 in [ 9 ] we can prove the following proposition: Proposition 1. Let I and J be two interpretations. Then J = TP (I) [ I if and only if vJ = H1(DP vI ) where H1 is applied element-wise.

Proposition 2. Let T P0 (I) = TP (I) [ I. Then T P0k(I) is a xed point for a large enough k. If sat(P [ I) then T P0k(I) = LHM (P [ I), otherwise T P0k(I) is inconsistent.

Hence, given a program P and an interpretation I, we can construct the corresponding matrix DP and vector vI . By repeatedly multiplying by DP and applying H1, we can compute a vector v corresponding to the xed point of T P0 (I). If P is satis able, by Proposition 2, v corresponds to the LHM (P [ I). Otherwise v1 = 1, meaning the interpretation includes ?.

An abductive task is a triplet < P; Ab; g >, where program P consists of background knowledge and constraints. Ab BP is a set of atoms called abducibles. g is an atom called an observation or goal term. We de ne an abductive solution to be a set Ab such that sat(P [ ) and g 2 LHM (P [ ). A solution is minimal if there does not exist 0 such that 0 is also an abductive solution. We are interested in nding minimal solutions of an abductive task. 3

Method

We rst de ne a single-step operator, the explanatory operator (EP ). This is similar in spirit to TP , and it allows us to generate abductive solutions in a \deductive" fashion. For simplicity, we assume Ab = BP . We will later consider ltering solutions according to a given speci c set of abducibles. The idea behind the explanatory operator is inverting implications. For instance, suppose P contains the rules fg q; g r; r s ^ tg. Then possible (minimal) explanations for g are fgg (since g 2 LHM (P [ fgg)), fqg, frg and fs; tg. To arrive at these solutions, our operator takes an interpretation such as fgg and for each rule with g as its head, creates a new interpretation consisting of the atoms in the body of that rule. So in the example above, the explanatory operator maps fgg to the two interpretations fqg and frg. An interpretation I generated in this manner may be inconsistent with the program (that is, unsat(P [ I)). So we remove from its output any interpretations that are inconsistent with P . The explanatory operator output includes I as well, as we would like to maintain solutions that we have already found as we repeatedly perform the operation. De nition 1. Let P be a program and I an interpretation such that sat(P [ I). The explanatory operator EP applied to I, denoted EP (I) is given by EP (I) = fIg [ Infhead(r)g [ body(r) r 2 P; head(r) 2 I \ I0 sat(P [ I0) To apply EP iteratively, we extend its de nition to E^P , which can be applied to a set of interpretations, I, all of which should be consistent with P . Then E^P (I) = S EP (I). We can now de ne the powers of E^P (I) by setting E^P0 (I) = I and IE2^In+1(I) = E^P (E^Pn (I)). For the program above, E^P0 (ffggg) =

P ffggg, E^P1 (ffggg) = ffgg; fqg; frgg, E^P2 (ffggg) = ffgg; fqg; frg; fs; tgg and E^P3 (ffggg) = E^P2 (ffggg). E^P2 (ffggg) is therefore a xed point. The next proposition ensures that a xed point will always be reached.

Proposition 3. Let I be a set of interpretations all consistent with a program P . Then there exists a smallest natural number n for which E^n+1(I) = E^Pn (I). P Proof. Note that, by the de nition of EP , for every I 2 I we have I 2 EP (I), meaning I E^P (I). By induction it follows that E^Pn (I) E^Pn+1(I). Hence jE^Pn (I)j is monotonically increasing in n. But for a nite program P , the Herbrand base BP is nite and therefore jE^Pn (I)j is bounded from above by 2jBP j. Therefore, there exists a smallest n for which E^Pn (I) = E^Pn+1(I). tu We denote the xed point by E^P (ffggg). A generic abductive algorithm would construct E^P (ffggg) by iteratively computing E^P over interpretations. This is connected to the relationship between abduction and Clark Completion [ 1 ]. Proposition 4. Suppose 2 E^P (ffggg). Then sat(P [ ) and g 2 LHM (P [ ) and is an abductive solution.

Proposition 4 shows that E^P (ffggg) contains only abductive solutions. Although it does not in general nd all solutions, it does contain all the minimal ones. To show this, we rst de ne a more general version of minimality.

De nition 2. Given an abductive task < P; Ab; g >, a solution minimal if g 2 TPn[ (;) and for every proper subset 0 ( is n-step we have g 62 TPn[ 0 (;). Intuitively, is n-step minimal if g can be derived from P [ in exactly n steps, and every atom in is necessary to do so. For example, consider the program P = fg p ^ q; p t; p qg. We have E^P (ffggg) = ffgg; fp; qg; ft; qg; fqgg. fp; qg is a solution that is not minimal, in fact it is 2-step minimal. fqg is a minimal solution that is not 2-step minimal, but is 3-step minimal. fq; tg is another solution that is not minimal, nor is it n-step minimal for any n. It is easy to see that all minimal solutions are n-step minimal for some natural number n. Proposition 5. Suppose that for the abductive task < P; BP ; g > we have that is an n-step minimal solution for some natural number n. Then 2 E^P (ffggg).

We now move from a generic algorithm to a linear algebraic one. First, we construct a third-order tensor which realises the E^P operator. Interpretations, as before, can be represented as vectors. To represent a set of interpretations, we simply stack these vectors as columns of a matrix. Using 2-mode multiplication [ 5 ] on this matrix with the tensor realises application of the E^P operator. This operation, however, does not produce quite the desired result. Firstly, there may be duplicate columns, which can simply be removed. More importantly, some of the columns will represent interpretations inconsistent with P . In essence, tensor multiplication will realise the following part of the EP operation: fIg [

Infhead(r)g [ body(r) r 2 P; head(r) 2 I . Luckily, we have a simple way to remove inconsistent solutions: We can compute the xed point for each column of the matrix using matrix multiplication as in Section 2. Filtering these out, we get exactly the behaviour of EP and achieve linear algebraic abduction.

In more detail, let P be a program with K 1 non-constraint rules such that BP has size N . We map a program P to an Abductive Tensor AP 2 RN N K . The rst K 1 frontal slices of AP correspond to its (inverted) rules. If the k th rule has head(r) = pj and body(r) = fpi1 ; pi2 ; :::; pim g then we set AP i2jk = ::: = AiPmjk = 1. This ensures that if pj is \turned on" in i1jk = AP an interpretation, then multiplication with this frontal slice will \turn on" the atoms in the body of the rule. We also set A1P1k = A2P2k = ::: = AP i 1;i 1;k = AiP+1;i+1;k = ::: = APN;N;k = 1, with all other elements set to 0 (note that AiP;i;k = 0). This will \turn o " pj while leaving all other atoms intact. We do this for all K 1 rules. Finally, the last slice is equal to the identity matrix A:P:K = I, and corresponds to keeping the current interpretation. As an example, consider the program P = fg q ^ r; q t; ? tg. The frontal slices of the corresponding tensor are: A:P:1 = Our generic algorithm can then be realised as follows: Given a program P and goal g, construct the tensor AP and matrix DP . For a set of interpretations I construct the corresponding matrix U I and then compute E^P (I) as follows. Let W = H1(AP 2 U I ), where duplicate columns are removed from W . Next compute the xed point for each column of W , using DP and the same method outlined in Section 2. The rst element of each column corresponds to ? and if set to 1 in the xed point it indicates the column can be removed since it represents an inconsistent interpretation. If we begin with I = ffggg and perform the above steps iteratively, we compute E^P (ffggg). We only need to ensure fgg is consistent with P . Each column of the nal matrix corresponds to an abductive solution, with all minimal solutions assured to be included. For example, for the above program the abductive process is as follows: 203 The matrix W is the xed point, its columns corresponding to fq; rg and fgg, while the column corresponding to fr; tg has been removed as it is inconsistent with the program. The next proposition ensures the correctness of the tensor representation.

Proposition 6. Let I be an interpretation consistent with a program P . Denote J = fIg [ Infhead(r)g [ body(r) r 2 P; head(r) 2 I . Let U = H1(AP 2 vI ). Then the columns of U correspond to the interpretations in J .

Finally, we consider the case where we have a general set of abducibles Ab BP . After computing E^P (ffggg) we can lter out solutions that are not a subset of Ab. Note that Ab if and only if v vAb = v where means element-wise multiplication. This is one such way to achieve post- ltering of solutions. Theorem 1. Given an abductive task < P; Ab; g >, the algorithm above produces a subset of the abductive solutions that contains all minimal solutions. Proof. Propositions 1 and 6 ensure that linear algebraic operations allow the computation of E^P (ffggg). Proposition 3 ensures the algorithm always halts and correctness can be seen from Propositions 4 and 5. 4

Discussion

We have introduced a linear algebraic approach to abduction in propositional Horn programs via an explanatory operator and outline the correctness of the approach. We have also provided a characterization of the operator by use of third-order tensors.

A straight-forward unoptimised implementation has been constructed and here we consider two possible optimisations: First, to prevent repeated computations, we can maintain a list of interpretations that have already been multiplied by the tensor. At each step of the algorithm we can remove columns from the interpretation matrix U I if they already appear in this list. Second, our tensor may be broken down to a sequence of tensors A1P ; A2P ; :::; AnP , each embedding rules that share the same head. Multiplying U I by each tensor in sequence will produce the same result but can create fewer duplicate columns. While nding abductive solutions in Horn propositional programs is NP-complete [ 3 ], our bottom-up approach together with the suggested optimisations can eliminate many unnecessary computational steps.

In the future, we plan to investigate extending our method to rst-order logic, for instance by combining it with Sato's tensor representation of Tarskian Semantics [ 10 ], initially starting with unary predicates. A second extension is to allow for normal logic programs P and exploit the connection between negationas-failure and abduction [ 4 ] to compute models under stable semantics.

References

1. Console , U. , Dupr , D. , Torasso , P. : On the relationship between abduction and deduction . Journal of Logic and Computation 1 ( 5 ), 661 { 690 ( 1991 ). https://doi.org/10.1093/logcom/1.5. 661

2. Corapi , D. , Russo , A. , Lupu , E.: Inductive Logic Programming in Answer Set Programming . In: Muggleton, S.H. , Others (eds.) Inductive Logic Programming . pp. 91 { 97 . Springer Berlin Heidelberg, Berlin, Heidelberg ( 2012 )

3. Eiter , T. , Gottlob , G. : The complexity of logic-based abduction . J. ACM 42 ( 1 ), 3 { 42 (Jan 1995 ). https://doi.org/10.1145/200836.200838

4. Eshghi , K. , Kowalski , R.: Abduction Compared with Negation by Failure . pp. 234 { 254 (01 1989 )

5. Kolda , T.G. , Bader , B.W. : Tensor Decompositions and Applications . SIAM REVIEW 51(3) , 455 { 500 ( 2009 )

6. Muggleton , S.H. , Lin , D. , Pahlavi , N. , Tamaddoni-Nezhad , A. : Meta-interpretive learning: application to grammatical inference . Machine Learning 94 ( 1 ), 25 {49 (Jan 2014 ). https://doi.org/10.1007/s10994-013-5358-3

7. Ray , O. : Nonmonotonic Abductive Inductive Learning . Journal of Applied Logic 7 ( 3 ), 329 { 340 ( 2009 ). https://doi.org/10.1016/j.jal. 2008 . 10 .007, special Issue : Abduction and Induction in Arti cial Intelligence

8. Rocktaschel, T., Riedel , S. : End-to-end di erentiable proving . In: Guyon, I. , Others (eds.) Advances in Neural Information Processing Systems 30 , pp. 3788 { 3800 . Curran Associates, Inc. ( 2017 )

9. Sakama , C. , Inoue , K. , Sato , T. : Linear Algebraic Characterization of Logic Programs . In: KSEM. Lecture Notes in Computer Science , vol. 10412 , pp. 520 { 533 . Springer ( 2017 ), https://doi.org/10.1007/978-3- 319 -63558-3_ 44

10. Sato , T. : Embedding Tarskian Semantics in Vector Spaces (Mar 2017 ), http:// arxiv.org/abs/1703.03193v1

11. Sera ni , L., Garcez , A.S.d.: Logic Tensor Networks: Deep Learning and Logical Reasoning from Data and Knowledge . CoRR abs/1606 .04422 ( 2016 )

12. van Emden, M.H. , Kowalski , R.A. : The Semantics of Predicate Logic as a Programming Language . Journal ACM 23 ( 4 ), 733 {742 (Oct 1976 )