Abstract fixpoint semantics and abstract procedural semantics of definite logic programs

A class of abstract interpretations of definite logic programs are discussed that are characterized by stable abstraction functions and a procedural characterization of the abstract fixpoint semantics is given. The authors give the notion of partial unification and define abstract fixpoint semantics. They then define a partial SLD resolution procedure over the concrete domain and relate it to the abstract fixpoint semantics by proving its soundness and completeness. They generalize the partial SLD resolution procedure, resulting in an abstract SLD resolution procedure over the abstract domain. They illustrate the computation of the abstract fixpoint semantics for depth abstractions and the application of the abstract SLD resolution procedure