Paper: Prop revisited: propositional formula as abstract domain for groundness analysis (at LICS 1991)

Authors: Agostino Cortesi Gilberto Filé William H. Winsborough

Abstract

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

BibTeX

  @InProceedings{CortesiFilWinsborou-Proprevisitedpropos,
    author = 	 {Agostino Cortesi and Gilberto Filé and William H. Winsborough},
    title = 	 {Prop revisited: propositional formula as abstract domain for groundness analysis },
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {322--327},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }