## A Kripke-Kleene semantics for logic programs.(English)Zbl 0589.68011

Familiar semantics for the Horn clause logic programs P is defined by a least fixed point of a monotone transformation $$\Phi_ P$$ defined on sets S of atomic statements. The intended interpretation is two-valued with members of S being true and remaining atomic statements false. The author proposes extension of this approach to the general case of logic programs consisting of arbitrary (not necessarily Horn) clauses. His operator $$\Phi_ P$$ keeps account both of truth (T) and falsity (F) of atomic statements A by operating on sets S of signed atomic statements TA, FA. A conjunction $$A_ 1\&...\&A_ k\&\neg B_ 1\&...\&\neg B_ m$$ is (by definition) made true by any S containing $$TA_ 1,...,TA_ k,\quad FB_ 1,...,FB_ m;$$ it is made false by any S containing some $$FA_ i$$ or $$TB_ j$$. Now $$S'=\Phi_ P(S)$$ is defined by the stipulation that $$TA\in S'$$ (resp. $$FA\in S')$$ if the premiss of some (resp. any) instance of some (resp. any) clause in P having the conclusion A is made true (resp. false) by S. Sets of signed statements form a complete semilattice (all infima and suprema of directed sets) under inclusion. Since $$\Phi_ P$$ is monotone, the least and other fixed point exist. It turns out that S is a fixed point of $$\Phi_ P$$ exactly when the ”if and only if” form of P [K. L. Clark, Negation as failure, in Logic and Data Bases, Plenum Press, New York, 293-322 (1978; Zbl 0412.68089)] is made true by S. All this is formulated in terms of three-valued logic and connected with Kripke’s approach to the treatment of partial predicates and truth-definitions. Usual relation between finite failure and maximal fixed points is also preserved. It is claimed that only programs P with $$\Phi_ P$$ continuous (in the sense of semilattice) should be considered acceptable.
Reviewer: G.Mints

### MSC:

 68Q60 Specification and verification (program logics, model checking, etc.) 68N01 General topics in the theory of software 68T99 Artificial intelligence

Zbl 0412.68089
Full Text: