Learning Acyclic First-order Horn Sentences From Entailment

This paper consider the problem of learning an unknown first-order Horn sentence H 3 from examples of Horn clauses that H 3 implies and 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) allow recursions, disjunctive definitions, and the use of function symbols. We present an algorithm that exactly identifies every target Horn program H 3 in ACH(k) in polynomial time in p; m and n using O(pmn k+1 ) entailment equivalence queries and O(pm 2 n 2k+1 ) request for a hint queries, where p is the number of predicates, m is the number of clauses contained in H 3 and n is the size of the longest counterexample. This algorithm combines saturation and least general generalization operators to invert resolution steps. Then, we show that request for hint queries can be replaced by entailment membership queries for a proper subclass of ACH(k). Using this method, we have a polynomi..