act Interpretation Framework for (almost) Full Prolog1 B. Le Charlier S. Rossi P. Van Hentenryck University of Namur University of Padova Brown University 21 rue Grandgagnage 7 via Belzoni Box 1910, Providence B-5000 Namur (Belgium) I-35131 Padova (Italy) RI 02912 (USA) abstract interpretation framework is introduced, which captures Prolog depth- rst strategy and the cut operation. The framework is based on a new conceptual idea, the notion of substitution s, and the traditional xpoint approach to abstract interpretation. It broadens the class ses that are amenable in practice to abstract interpretation and re nes the precision of existing analyses. Its practicability is demonstrated in a companion paper 4]. This paper focuses on theoretical foundations.