Resolution for skeptical stable semantics

Abstract

An extension of resolution for skeptical stable model semantics is introduced. Unlike previous approaches, our calculus often needs to consider only a strict subset of the program rules. Moreover, we characterize a large class of programs whose derivations may proceed in a thoroughly goal-directed way. Some inferences, which depend on non-ground negative goals, can be drawn without resorting to negation-as-failure; as a consequence, many goals which flounder in the standard setting, have a successful skeptical derivation. The paper contains a preliminary study of some interesting derivation strategies.