WITOLD LUKASZEWICZ AND ANDRZEJ SZA LAS

Abstract. In recent years, a great deal of attention has been devoted to logics of common-sense reasoning. Among the candidates proposed, circumscription has been perceived as an elegant mathematical technique for modeling non-monotonic reasoning, but dicult to apply in practice. The major reason for this is the second-order nature of circumscription axioms and the diculty in nding proper substitutions of predicate expressions for predicate variables. One solution to this problem is to compile, where possible, second-order formulas into equivalent rst-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 certain circumscription axioms to rst-order formulas. The algorithm takes as input an arbitrary second-order formula and either returns as output an equivalent rst-order formula, or terminates with failure. The class of second-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 quantiers (some involving Skolemization), variable constants, non-separated formulas, and formulas with n-ary predicate variables. In addition, we analyze the strength of the algorithm, compare it with existing approaches, and provide formal subsumption results