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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, E-ISSN 1875-8681, Vol. 28, no 3,4, p. 261-272Article 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, p. 261-272
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-41621DOI: 10.3233/FI-1996-283404Scopus ID: 2-s2.0-0030383468Local ID: 58414OAI: oai:DiVA.org:liu-41621DiVA, id: diva2:262475
Available from: 2009-10-10 Created: 2009-10-10 Last updated: 2018-01-12

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Doherty, PatrickLukaszewicz, WitoldSzalas, Andrzej

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 Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 169 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf