Abstract: Abstract interpretation is a general theory of semantics approximation, which has been widely used in the verification of computer programs. Existing abstract interpretation based verification methods for logic programs do not deal with the properties ass

Key words: Abstract interpretation, Program verification, Prolog, Fixpoint semantics