A reduction result for circumscribed semi-horn formulas
1996 (English)In: Fundamenta Informaticae, ISSN 0169-2968, Vol. 28, no 3,4, 261-272Article in journal (Refereed) Published
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 Ackermann's Lemma in order to deal with a subclass of universal formulas called semi-Horn formulas. Our results subsume previous results by Kolaitis and Papadimitriou regarding a characterization of circumscribed definite logic programs which are first-order expressible. The method for distinguishing which formulas are reducible is based on a boundedness criterion. The approach we use is to first reduce a circumscribed semi-Horn formula to a fixpoint formula which is reducible if the formula 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.
National CategoryComputer Science
IdentifiersURN: urn:nbn:se:liu:diva-41621DOI: 10.3233/FI-1996-283404ScopusID: 2-s2.0-0030383468Local ID: 58414OAI: oai:DiVA.org:liu-41621DiVA: diva2:262475