# An Application Of Proof-Theory In Answer Set Programming

V. W. Marek Department of Computer Science University of Kentucky Lexington, KY 40506 J.B. Remmel Departments of Computer Science and Mathematics University of California La Jolla, CA 92093 November 2, 2021

## Abstract 1

Using a characterization of stable models of logic programs P as satisfying valuations of a suitably chosen propositional theory, called the set of reduced defining equations rΦP , we show that the finitary character of that theory rΦP is equivalent to a certain continuity property of the GelfondLifschitz operator GLP associated with the program P.

We discuss possible extensions of techniques proposed in this paper to the context of cardinality constraints.

## 1 Introduction

The use of proof theory in logic based formalisms for constraint solving is pervasive. For example, in Satisfiability (SAT), proof theoretic methods are used to find lower bounds on complexity of various SAT algorithms. However, prooftheoretic methods have not played as prominent role in Answer Set Programming
(ASP) formalisms. This is not to say that there were no attempts to apply prooftheoretic methods in ASP. To give a few examples, Marek and Truszczynski in
[MT93] used the proof-theoretic methods to characterize Reiter's extensions in arXiv:0905.0197v2 [cs.AI] 11 Jan 2010