This article gives an informal, soft introduction to our paper "Efficient Program Synthesis Using Constraints in Inductive Logic Programming". Inverse Entailment is an induction method used in inductive logic programming (ILP). To understand how inverse entailment works, consider the following unrestricted ILP search for a grandparenthood definition: The top candidate (node) contains the hypothesis grandparent(_,_), which means "everybody is a grandparent of everybody". By using inverse entailment, we can also have a bottom candidate, called the bottom clause. It is the most specific hypothesis, from which all other candidates may be generated: We do this by giving rules of the form "if a candidate has body literal 1 and 3, it should not have literal 5". Here we can directly refer to the literals by numbers (literal 1, 3 and 5) since we have explicitly constructed the bottom clause, which lists all possible literals. For example, we could require that the parent/2 predicate takes a parent as input and outputs all children. Likewise, grandparent takes a grandparent as input and outputs all grandchildren. Since grandparent/2 must then use a definition that computes its second argument (grandchildren), and the use of parent/2 requires its first argument to be pre-computed (instantiated), we get a set of input-output constraints, which eliminates many candidates. For example: - grandparent(_,_) is not a viable candidate since it does not compute grandchildren.
- grandparent(A,_) :- parent(A,_) is not viable for the same reason: it does not compute the second argument to grandparent/2.
- grandparent(_,A) :- parent(_,A) does compute grandchildren (A), but is not viable because parent/2 has uninstantiated input.
After eliminating non-viable candidates, we obtain the following graph, where non-viable candidates have been crossed out: That is, there are only two candidates that are viable; hence only two candidates that need to be evaluated. The correct definition is the upper one: grandparent(A,B) :- parent(A,C), parent(C,B). This reduction of search space was obtain using input-output constraints, which are declared in mode declarations (modeh and modeb): :- modeh(*, grandparent(+person, -person))? :- modeb(*, parent(+person, -person))? Another type of constraint is pruning constraints, which prune all generalizations of inconsistent candidates (since they are inconsistent too), and all specializations of consistent candidates (since they never cover more positive examples). These constraints are dynamically generated by the Atom system after evaluating each candidate. For example, if we evaluated the correct solution first, then there would be no need to evaluate the bottom clause itself; the bottom clause would be pruned away by pruning constraints. A third type of constraint is functional constraints, used with predicates who always evaluate to true, or for which we don't care about it's predicate evaluation. For example, arithmetic multiplication always succeeds and hence is declared functional: :- modeb(1, -int is +int * +int, [functional])? Other predicates which can be considered functional are list operations: splitting, constructing, sorting, rotating, etc. That is, most program synthesis predicates are functional. Examples of non-functional predicates are those that check some condition: is_empty(+list), is_sorted(+list), is_even(+int). Functional constraints require that at least one output of a functional literal is used elsewhere in the clause; otherwise there is no point in having the literal (as its truth-value has been declared uninteresting). Although parent/2 is not supposed to be a functional predicate, if it were declared as such, the bottom clause itself would not be a viable candidate since its last literal, parent(B,_), does not make use of the output. A fourth type of constraints are equality constraints generated during variable splitting (see paper for more details). Finally, domain specific constraints can be generated. For example, since X ≤ X for any X, we may prune all bottom clause literals of this form. This is an unconditional removal of a literal, and doesn't require constraints (the constraint is simply a unit clause { ¬b3 }): :- prevent X =< X? Now consider transitivity: if A ≤ B and B ≤ C, then A ≤ C: :- A =< B, B =< C => A =< C? This generates a constraint b3∧b5 ⇒ b8, or equivalently, {¬b3, ¬b5, ¬b8 }, for which no literal can be removal without dynamically checking constraints during search (that is, we need the framework of Constrained Inverse Entailment). Links: |

research >