Learning acyclic first-order horn sentences from entailment

Abstract

This paper considers the problem of learning an unknown first-order Horn sentence H. from examples of Horn clauses that H. either implies or does not imply. Particularly, we deal with a subclass of first-order Horn sentences ACH(k), called acyclic constrained Horn programs of constant arity k. ACH (k) allows recursions, disjunctive definitions, and the use of function symbols. We present an algorithm that exactly identifies every target Horn program H. in ACH(k) in polynomial time in p, m and n using O(pmnk+l) entailment equivalence queries and O(pm2n2k+l) request for hint queries, where p is the number of predicates, m is the number of clauses contained in H. and n is the size of the longest counterexample. This algorithm combines saturation and least general generalization operators to invert resolution steps. Next, using the technique of replacing request for hint queries with entailment membership queries, we have a polynomial time learning algorithm using entailment equivalence and entailment membership queries for a subclass of ACH(k). Finally, we show that any algorithm which learns ACH(k) using entailment equivalence and entailment membership queries makes Ω (mnK) queries, and that the use of entailment cannot be eliminated to learn ACH(k) even with both equivalence and membership queries for ground atoms are allowed.