BOTTOM-UP ABSTRACT INTERPRETATION OF LOGIC PROGRAMS

This paper presents a formal framework for the bottom-up abstract inte rpretation of logic programs which can be applied to approximate answe r substitutions, partial answer substitutions and call patterns for a given program and arbitrary initial goal. The framework is based on a T (p)-like semantics defined over a Herbrand universe with variables w hich has previously been shown to determine the answer substitutions f or arbitrary initial goals. The first part of the paper reconstructs t his semantics to provide a more adequate basis for abstract interpreta tion. A notion of abstract substitution is introduced and shown to det ermine an abstract semantic function which for a given program can be applied to approximate the answer substitutions for an arbitrary initi al goal. The second part of the paper extends the bottom-up approach t o provide approximations of both partial answer substitutions and call patterns. This is achieved by applying Magic Sets and other existing techniques to transform a program in such a way that the answer substi tutions of the transformed program correspond to the partial answer su bstitutions and call patterns of the original program. This facilitate s the analysis of concurrent logic programs (ignoring synchronization) and provides a collecting semantics which characterizes both success and call patterns.