Derivation Procedures for Extended Stable Models

Abstract

We present derivation proof procedures for extended stable model semantics. Given program \\Pi and goal G, G belongs to the well founded model of \\Pi iff there is a WFM-derivation for G in \\Pi. Likewise, given program \\Pi and goal G, G belongs to some extended stable model of \\Pi iff there is a XSM-derivation for G in \\Pi. Correctness (completeness and soundness) of these procedures is discussed. Example derivations are exhibited, as well as a simple Prolog implementation that directly mirrors the procedures. 1 Introduction Well Founded Semantics (WFS) [ Van Gelder et al., 1990 ] adequately captures various forms of hypothetical reasoning [ Pereira et al., 1991c, Pereira et al., 1991d, Pereira et al., 1991b, Pereira et al., 1991a ] if we interpret the well-founded model (WFM) of a program \\Pi as a (possibly incomplete) core view of the world, the extended stable models (XSMs) specifying alternative complementary consistent views of the world, all of each containing the core WFM . The...