Abductive Analysis of Modular Logic Programs

We introduce a practical method for abductive analysis of modular logic programs. This is obtained by reversing the deduction process, which is usually applied in static-dataflow analysis of logic programs. The approach is validated in the framework of abstract interpretation. The abduced information provides an abstract specification for program modules which can be of assistance both in top-down development of programs and in compile-time optimization. To the best of our knowledge this is the first application of abductive reasoning in dataflow analysis of logic programs. 1 Introduction Dataflow analysis by abstract interpretation is typically intended to statically derive approximated information (the analysis) about run-time properties of programs, by applying rules (clauses) to initial states (goals), with the inference of a result. This deductive approach to logic program analysis is usually based on abstract unfolding (i.e. replacement + abstract unification).