@TECHREPORT{R-95-20,
PSURL = {/publications/cgi-bin/tr-fetch.pl?r-95-20+ps},
NUMBER = {R-95-20},
INSTITUTION = ida,
ADDRESS = idaaddr,
YEAR = {1995},
AUTHOR = {Doherty, Patrick and Lukaszewicz, Witold and Salas, Andrzej},
TITLE = {A Characterization Result for Circumscribed Normal Logic Programs},
ABSTRACTURL = {/publications/cgi-bin/tr-fetch.pl?r-95-20+abstr},
ABSTRACT = {Circumscription has been perceived as an elegant mathematical technique for modeling nonmonotonic and commonsense reasoning, but difficult to apply in practice due to the use of second-order formulas. One proposal for dealing with the computational problems is to identify classes of first-order formulas whose circumscription can be shown to be equivalent to a first-order formula. In previous work, we presented an algorithm which reduces certain classes of second-order circumscription axioms to logically equivalent first-order formulas. The basis for the algorithm is an elimination lemma due to Ackermann. In this paper, we capitalize on the use of a generalization of the Ackermann lemma in order to deal with a subclass of universal formulas used in normal logic programs. Our results subsume previous results by Kolaitis and Papadimitriou regarding a characterization of circumscribed definite logic programs which are first-order expressible. The means for distinguishing which programs are reducible is based on a boundedness criterion. The approach we use is to first reduce circumscribed normal logic programs to a fixpoint formula which is reducible if the program is bounded, otherwise not. In addition to a number of other extensions, we also present a fixpoint calculus which is shown to be sound and complete for bounded fixpoint formulas.}