liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
A reduction result for circumscribed semi-horn formulas
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab.
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab.
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab.
1996 (English)In: Fundamenta Informaticae, ISSN 0169-2968, Vol. 28, no 3,4, 261-272 p.Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
IOS Press , 1996. Vol. 28, no 3,4, 261-272 p.
National Category
Computer Science
Identifiers
URN: urn:nbn:se:liu:diva-41621DOI: 10.3233/FI-1996-283404ScopusID: 2-s2.0-0030383468Local ID: 58414OAI: oai:DiVA.org:liu-41621DiVA: diva2:262475
Available from: 2009-10-10 Created: 2009-10-10 Last updated: 2011-02-27

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Doherty, PatrickLukaszewicz, WitoldSzalas, Andrzej
By organisation
The Institute of TechnologyKPLAB - Knowledge Processing Lab
In the same journal
Fundamenta Informaticae
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 105 hits
ReferencesLink to record
Permanent link

Direct link