Abstract fixpoint semantics and abstract procedural semantics of definite logic programs

Author

Lu, Lunjin ; Greenfield, Peter

Author_Institution

Sch. of Comput. Sci., Birmingham Univ., UK

fYear

1992

fDate

20-23 Apr 1992

Firstpage

147

Lastpage

154

Abstract

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

Keywords

formal logic; logic programming; system monitoring; abstract SLD resolution procedure; abstract fixpoint semantics; abstract interpretations; completeness; concrete domain; definite logic programs; depth abstractions; partial SLD resolution procedure; partial unification; procedural characterization; soundness; stable abstraction functions; Computational modeling; Computer science; Concrete; Logic; Scholarships; Solids; Superluminescent diodes;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Languages, 1992., Proceedings of the 1992 International Conference on

Conference_Location

Oakland, CA

Print_ISBN

0-8186-2585-6

Type

conf

DOI

10.1109/ICCL.1992.185477

Filename

185477