Deriving Abstract Semantics for Forward Analysis of Normal Logic Programs

1998/11/06 by Lunjin Lu, Lu, Lunjin
Computer Science · #D.3.2 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)

paper · pdf · doi:10.48550/arxiv.cs/9811012

openalex publication_date 1998/11/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

The problem of forward abstract interpretation of \em normal logic programs has not been formally addressed in the literature although negation as failure is dealt with through the built-in predicate ! in the way it is implemented in Prolog. This paper proposes a solution to this problem by deriving two generic fixed-point abstract semantics F^b and F^\diamond for forward abstract interpretation of \em normal logic programs. F^b is intended for inferring data descriptions for edges in the program graph where an edge denotes the possibility that the control of execution transfers from its source program point to its destination program point. F^\diamond is derived from F^b and is intended for inferring data descriptions for textual program points.

Related

• Towards a Systematic Account of Different Semantics for Logic Programs
• Graph-based Interpretation of Normal Logic Programs
• A Well-Founded Semantics for FOL-Programs
• Corollaries on the fixpoint completion: studying the stable semantics by means of the Clark completion
• Abstract Interpretation as a Programming Language