A Freeness and Sharing Analysis of Logic Programs Based on a Pre-interpretation

. Recently, a technique was presented for using pre-interpretations for abstract interpretation of the correct answer set CP of a logic program P . So far it was an open problem whether pre-interpretations could also be used for deriving non-downward closed properties of the computed answer set OP such as definite freeness. This paper shows that it is possible to do so. 1 Introduction Cousot and Cousot [13, 14] have developed a widely applicable framework for abstract interpretation and obtained the following basic result: if an abstract operator ¯ A over an abstract domain Dom A of data descriptions fl-approximates a corresponding concrete operator ¯ C over a concrete domain Dom C of data elements, and both operators are monotonic functions, then the fixpoints of both operators are such that lfp(¯ A ) fl-approximates lfp(¯ C ). For logic programs, the concrete operator ¯ C can be a bottom-up semantic function or a top-down one. In both cases, the execution essentially..