LiU Electronic Press
Full-text not available in DiVA
Author:
Doherty, Patrick (Linköping University, The Institute of Technology) (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab)
Lukaszewicz, Witold (Linköping University, The Institute of Technology) (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab)
Szalas, Andrzej (Linköping University, The Institute of Technology) (Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab)
Title:
Computing circumscription revisited: A reduction algorithm.
Department:
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab
Linköping University, The Institute of Technology
Publication type:
Report (Other academic)
Language:
English
Place of publ.: Linköping, Sweden Publisher: Department of Computer and Information Science, Linköping University
Series:
LITH-IDA-R, ISSN 0281-4250; 94-42
Year of publ.:
1994
URI:
urn:nbn:se:liu:diva-41719
Permanent link:
http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-41719
ISRN:
LITH-IDA-R-94-42
Local ID:
58857
Subject category:
Computer Science
SVEP category:
Computer science
Abstract(en) :

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 nd-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, nd-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.

Available from:
2009-10-10
Created:
2009-10-10
Last updated:
2012-02-13
Statistics:
13 hits