We study the application of abstract interpretation to the design of inductive methods for verifying properties of logic programs.
We give a unified view of inductive assertion-based proof methods for logic programs, by systematically deriving them in a
uniform way using Abstract Interpretation. The resulting verification framework allows us to reconstruct several existing
verification methods and to understand the relation among them in terms of abstractions. Moreover, we can tackle the problem
of establishing the completeness of the proof methods.
Keywords Inductive proof methods - abstract interpretation - abstract domains