PROP REVISITED - PROPOSITIONAL FORMULA AS ABSTRACT DOMAIN FOR GROUNDNESS ANALYSIS

The abstract domain Prop for analyzing variable groundness in logic programs is considered. This domain consists of (equivalence classes of) propositional formulas whose propositional variables correspond to program variables with truth assignments indicating which program variables are ground. Some ambiguity remains about precisely which formula should be included in Prop so that all interesting sets of program execution states (substitutions) have a unique representation. This ambiguity is clarified by characterizing, both semantically and syntactically, the appropriate definition of Prop. The use of propositional formulas for representing properties of substitutions of a different type than groundness, such as freeness and independence of variables, is discussed.