An Abstraction of Fixpoint Semantics for Normal Logic Programs


IEICE TRANSACTIONS on Information and Systems   Vol.E79-D   No.3   pp.196-208
Publication Date: 1996/03/25
Online ISSN: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Software Theory
logic program,  substitution manipulations,  fixpoint theory,  abstract interpretation,  

Full Text: PDF>>
Buy this Article

We deal with a fixpoint semantics for normal logic programs by means of an algebraic manipulation of idempotent substitution sets. Because of the negation, the function associated with a given normal logic program, which captures the deductions caused by the program, is in general nonmonotonic, as long as we are concerned with 2-valued logic approach. The demerit of the nonmonotonic function is not to guarantee its fixpoint well, although the fixpoint is regarded as representing the whole behaviour. The stable model as in [6] is fixpoint of nonmonotonic functions, but it is referred to on the assumption of its existences. On the other hand, if we take 3-valued logic approach for normal logic programs as in [5], [9], [11], [14] we have the monotonic function to represent resolutions and negation as failure, and define its fixpoint well, if we permit the fixpoint not to be constructive because of discontinuity. Since the substituitions for variables in the program are essentially significant in the deductions for logic programming, we next focus on the representations by means of substitutions for the deductions, without usual expressions based on atomic formulas. We examine the semantics in terms of abstract interpretations among semantics as surveyed in [9], where an abstraction stands for the capability of representing another semantics. In this paper, in 3-valued logic approach and by means of the substitution manipulation, the semantics is defined to be an abstraction of the semantics in [5], [9]. To construct a semantics based on the idempotent substitution set, the algebraic manipulation of substitutions is significant, whereas the treatment in [10] for the case of definite clause sets is not available because of the restriction of substitutions to some variable domain as most general unifications.