RULES AS ACTIONS - A SITUATION CALCULUS SEMANTICS FOR LOGIC PROGRAMS

We propose a novel semantics for logic programs with negation by viewi ng the application of a clause in a derivation as an action in the sit uation calculus. Program clauses are then identified with situation ca lculus effect axioms as they are understood in axiomatic theories of a ctions. We then solve the frame problem for these effect axioms using a recent approach of Reiter [21], and identify the resulting collectio n of axioms with the semantics of the original logic problem. An inter esting consequence of this approach is that the logic programming nega tion-as-failure operator inherits its nonmonotonicity from the nonmono tonicity associated with the frame problem. One advantage of our propo sal is that like Clark's completion semantics, ours is also formulated explicitly in classical logic. To illustrate the usefulness of our se mantics, we prove sufficient conditions for two logic programs to be e quivalent, and use this to verify the correctness of the well-known un folding program transformation operator. We also discuss applications of this framework to formalizing search control operators in logic pro gramming. (C) Elsevier Science Inc., 1997.