AFP Algorithm and a Canonical Normal Form for Horn Formulas
This work addresses incremental improvements in computational learning theory for logic-based systems, with potential applications in AI and formal verification.
The paper tackles the problem of learning Horn formulas by analyzing the AFP Algorithm, showing that performing multiple refinements per negative counterexample does not improve its complexity, and introduces a canonical normal form for Horn formulas, proving the algorithm's output adheres to this form.
AFP Algorithm is a learning algorithm for Horn formulas. We show that it does not improve the complexity of AFP Algorithm, if after each negative counterexample more that just one refinements are performed. Moreover, a canonical normal form for Horn formulas is presented, and it is proved that the output formula of AFP Algorithm is in this normal form.