Abstracting s-semantics using a model-theoretic approach

© Springer-Verlag Berlin Heidelberg 1994. A new approach for abstract interpretation of definite logic programs is introduced. The basic idea is to use an equality theory which safely approximates the Free Equality theory. The non-Herbrand model generated from this theory is used for safely approximating the s-semantics of definite logic programs. By taking equality theories which enforce so called non-terms elements to appear in the domain, one can obtain approximate s-models which encode non declarative properties of computed answer substitutions such as freeness. It is possible to formulate equality theories which lead to several well known abstract domains.status: publishe