A significant extension of logic programming by adapting model building rules

Abstract

A method by the authors for automated model building is extended and specialized in a natural way in order to increase the possibilities of logic programming. A rather complete, though reasonably short, description of the ideas and technicalities of the former method is given in order to make the paper self-contained. Specialization of several key rules permits to obtain three main theoretical results concerning extensions of logic programming: non-ground negative facts as well as inductive consequences can be deduced from programs. Goals containing negations, quantifications and logical connectives are allowed. It is proven that the proposed extension is strictly more powerful than SLDNF. Several non-trivial running examples show evidence of the interest of our approach. Last but not least, a nice side effect exploits the model building capabilities of the approach: it is shown on one representative example how the method can be used to detect (and to correct) errors in logic programs. Main lines of future research are given.