Sökning: WFRF:(Szalas Andrzej 1956 ) >
A reduction result ...
A reduction result for circumscribed semi-horn formulas
-
- Doherty, Patrick, 1957- (författare)
- Linköpings universitet,Tekniska högskolan,KPLAB - Laboratoriet för kunskapsbearbetning
-
- Lukaszewicz, Witold, 1947- (författare)
- Linköpings universitet,Tekniska högskolan,KPLAB - Laboratoriet för kunskapsbearbetning
-
- Szalas, Andrzej, 1956- (författare)
- Linköpings universitet,Tekniska högskolan,KPLAB - Laboratoriet för kunskapsbearbetning
-
(creator_code:org_t)
- IOS Press, 1996
- 1996
- Engelska.
-
Ingår i: Fundamenta Informaticae. - : IOS Press. - 0169-2968 .- 1875-8681. ; 28:3,4, s. 261-272
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.3...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Computer science
- Datavetenskap
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas