**Dept. of Computer and Information science, Linköping University**

## IDA Technical Reports: abstract

*Generated: Sat, 31 Jan 2015 18:39:59 *

Doherty, P., Lukaszewicz, W., and Szalas, A. (1994).
** Computing
Circumscription Revisited: A Reduction Algorithm**.
Technical Report LiTH-IDA-R-94-42, Department of Computer and Information
Science, Linköping University, Sweden.
(bibtex),

**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.

**Goto (at Linköping University):**
```
CS Dept
TR Overview
```

*<webmaster@ida.liu.se>*