@techreport{R-94-42,
PSURL = {/publications/cgi-bin/tr-fetch.pl?r-94-42+ps},
ABSTRACTURL = {/publications/cgi-bin/tr-fetch.pl?r-94-42+abstr},
ABSTRACT = {In recent years, a great deal of attention has been devoted to logics of
"commonsense" reasoning. Among the candidates proposed, circumscription
has been perceived as an elegant mathematical technique for modeling
nonmonotonic reasoning, but difficult to apply in practice. The major
reason for this is the 2nd-order nature of circumscription axioms and
the difficulty in finding proper substitutions of predicate expressions
for predicate variables. One solution to this problem is to compile,
where possible, 2nd-order formulas into equivalent 1st-order formulas.
Although some progress has been made using this approach, the results
are not as strong as one might desire and they are isolated in nature.
In this article, we provide a general method which can be used in an
algorithmic manner to reduce circumscription axioms to 1st-order
formulas. The algorithm takes as input an arbitrary 2nd-order formula
and either returns as output an equivalent 1st-order formula, or
terminates with failure. The class of 2nd-order formulas, and analogously
the class of circumscriptive theories which can be
reduced, provably subsumes those covered by existing results.
We demonstrate the generality of the algorithm using
circumscriptive theories with mixed quantifiers (some involving Skolemization),
variable constants, non-separated formulas, and formulas with n-ary predicate
variables. In addition, we analyze the strength of the algorithm and compare
it with existing approaches providing formal subsumption results.
},
TITLE = {Computing Circumscription Revisited: A Reduction Algorithm},
AUTHOR = {Patrick Doherty and Witold Lukaszewicz and Andrzej Szalas},
EMAIL = {patdo@ida.liu.se},
YEAR = {1994},
NUMBER = {R-94-42},
INSTITUTION = ida,
ADDRESS = idaaddr,
IDANR = {LiTH-IDA-R-94-42},
NOTE = {}