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

Fitting, Melvin

J. Logic Program. 2, 295-312 (1985).

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

Keywords:

logic programming; semantics; Horn clause logic programs; fixed point; monotone transformation; three-valued logic

Citations:

Zbl 0412.68089