# Guarded Resolution For Answer Set Programming

V.W. Marek Department of Computer Science, University of Kentucky, Lexington, KY 40506 (**e-mail:** marek@cs.uky.edu)
J.B. Remmel Departments of Mathematics and Computer Science, University of California at San Diego, La Jolla, CA 92903 (**e-mail:** jremmel@ucsd.edu ) ∗
submitted 24 April 2009; revised 15 November 2009; accepted **1 January 2010**

## Abstract

We investigate a proof system based on a **guarded resolution rule** and show its adequacy for stable semantics of normal logic programs. As a consequence, we show that GelfondLifschitz operator can be viewed as a proof-theoretic concept. As an application, we find a propositional theory EP whose models are precisely stable models of programs. We also find a class of propositional theories CP with the following properties. Propositional models of theories in CP are precisely stable models of P, and the theories in CT are of the size linear in the size of P.

KEYWORDS: Guarded Resolution, Proof-theory for Answer Set Programming

## 1 Introduction

In this note, we introduce a rule of proof, called guarded unit resolution**. Guarded**
unit resolution is a generalization of a special case of the resolution rule of proof, namely, positive unit resolution**. In positive unit resolution, one of the inputs is an**
atom unit clause. Positive unit resolution is complete for Horn clauses, specifically, given a consistent Horn theory T and an atom p, the atom p **belongs to the least**
model of T , lm(T ), if and only if there is a positive unit resolution proof of p **from**
T **(Dowling and Gallier 1984).**
The modification we introduce in this note concerns guarded atoms and guarded Horn clauses. Guarded atoms are strings of the form: p : {r1, . . . , rm} **where**
p, r1, . . . , rm **are propositional atoms. Guarded Horn clauses are strings of the** form p ← q1, . . . , qn : {r1, . . . , rm} again with p, q1, . . . , qn, r1, . . . , rm **propositional**
atoms.

These guarded atoms and guarded rules will be used to obtain a characterization arXiv:0904.3953v4 [cs.AI] 21 Feb 2010
∗ Partially supported by NSF grant DMS 0654060.