Prop revisited: propositional formula as abstract domain for groundness analysis

Published 10 December 2002

Agostino Cortesi, G. Filé, William H. Winsborough

DOI10.1109/lics.1991.151656

Citations86

TL;DR

The abstract domain Prop for analyzing variable groundness in logic programs is considered and 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.

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.>

Keywords

Computer Science

Abstract interpretation

6,131 Citations1977Patrick Cousot, Radhia Cousot

The Complexity of Boolean Functions

883 Citations1987Ingo Wegener

Graduate texts in mathematicsA Course in Mathematical Logic

547 Citations1977Yu. I. Manin

Provability - introduction to formal languages truth and deducibility the continuum problem and forcing the continuum Problem and constructible sets computability - recursive functions and Church's thesis diophantine sets and algorithmic undecidability provability and computability Goedel's incompleteness theorem recursive groups.

Information and Software TechnologyAbstract interpretation of declarative languages

321 Citations1988Samson Abramsky, Chris Hankin +1 more

Book of abstract interpretation of declarative languages, as an amazing reference becomes what you need to get, when you have no idea about this book, it will be better for you to try reading this book.

View PDF

Choice Reviews OnlineA course on mathematical logic

257 Citations2008

This chapter discusses first-Order Logic, which is concerned with the construction of Boolean Algebras, and its application to Mathematical Logic.

The Journal of Logic ProgrammingA practical framework for theabstract interpretation of logic programs

250 Citations1991Maurice Bruynooghe

This work develops a general framework which is suited to develop complex applications and to prove their correctness, and presents a generic abstract interpretation procedure for the construction of such an abstract and-or graph.

View PDF

ACM Transactions on Programming Languages and SystemsStatic inference of modes and data dependencies in logic programs

138 Citations1989Saumya Debray

This paper describes and proves correct an algorithm for the static inference of modes and data dependencies in a program and is shown to be quite efficient for programs commonly encountered in practice.

View PDF

Notes for a Tutorial on Abstract Interpretation of Logic Programs

49 Citations1989Kim Marriott, Harald Søndergaard

interpretation formalizes the idea of approximate computation in which computation is performed with descriptions of data rather than the data itself, which means that the result it yields is not, in general, as precise as those of the proper computation.

Abstract interpretation of logic programs

36 Citations1991Agostino Cortesi, G. Filé

An abstract domain for the Abstract Interpretation of logic programs synthesizes the following properties of substitutions: groundless, sharing, freeness, covering, equivalence and compoundness of variables.