Abstract
We first define general domain circumscription (GDC) and provide it with a semantics. GDC subsumes existing domain circumscription proposals in that it allows varying of arbitrary predicates, functions, or constants, to maximize the minimization of the domain of a theory. We then show that for the class of semi-universal theories without function symbols, that the domain circumscription of such theories can be constructively reduced to logically equivalent first-order theories by using an extension of the DLS algorithm, previously proposed by the authors for reducing second-order formulas. We also isolate a class of domain circumscribed theories, such that any arbitrary second-order circumscription policy applied to these theories is guaranteed to be reducible to a logically equivalent first-order theory. In the case of semi-universal theories with functions and arbitrary theories which are not separated, we provide additional results, which although not guaranteed to provide reductions in all cases, do provide reductions in some cases. These results are based on the use of fixpoint reductions.
Supported in part by the Swedish Council for Engineering Sciences (TFR).
Supported in part by KBN grant 3 P406 019 06.
Supported in part by KBN grant 3 P406 019 06.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ackermann, W. (1935) Untersuchungen über das Eliminationsproblem, der mathematischen Logik, Mathematische Annalen, 110, 390–413.
Davis, M. (1980) The Mathematics of Non-Monotonic Reasoning, Artificial Intelligence J., 13, 73–80.
Doherty, P., Łukaszewicz, W., Szałas, A. (1994) Computing Circumscription Revisited. A Reduction Algorithm, Technical Report LiTH-IDA-R-94-42, Linköping University, 1994. Also in, Proc. 14th IJCAI, 1995, Montreal, Canada.8 Full version to appear in Journal of Automated Reasoning.9
Doherty, P., Łukaszewicz. W., Szałas, A. (1995) A Reduction Result for Circumscribed Semi-Horn Formulas, To appear in Fundamenta Informaticae, 1996.
Doherty, P., Łukaszewicz, W., Szałas, A. (1995) General Domain Circumscription and its First-Order Reduction, Technical Report LiTH-IDA-R-96-01, Linköping University.
Etherington, D. W., Mercer, R. (1987) Domain Circumscription: A Revaluation, Computational Intelligence, 3, 94–99.
Hintikka, J. (1988) Model Minimization — An Alternative to Circumscription, Journal of Automated Reasoning, 4, 1–13.
Lorenz, S. (1994) A Tableau Prover for Domain Minimization, Journal of Automated Reasoning, 13, 375–390.
Łukaszewicz, W. (1990) Non-Monotonic Reasoning — Formalization of Commonsense Reasoning, Ellis Horwood Series in Artificial Intelligence. Ellis Horwood, 1990.
McCarthy, J. (1977) Epistemological Problems of Artificial Intelligence, in: Proc. 5th IJCAI, Cambridge, MA, 1977, 1038–1044.
Nonnengart, A., Szałas, A. (1995) A Fixpoint Approach to Second-Order Quantifier Elimination with Applications to Correspondence Theory, Report of Max-Planck-Institut für Informatik, MPI-I-95-2-007, Saarbrücken, Germany.
Suchanek, M. A. (1993) First-Order Syntactic Characterizations of Minimal Entailment, Domain-Minimal Entailment, and Herbrand Entailment, Journal of Automated Reasoning, 10, 237–263.
Szałas, A. (1993) On the Correspondence Between Modal and Classical Logic: an Automated Approach, Journal of Logic and Computation, 3, 605–620.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Doherty, P., Łukaszewicz, W., Szałas, A. (1996). General domain circumscription and its first-order reduction. In: Gabbay, D.M., Ohlbach, H.J. (eds) Practical Reasoning. FAPR 1996. Lecture Notes in Computer Science, vol 1085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61313-7_65
Download citation
DOI: https://doi.org/10.1007/3-540-61313-7_65
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61313-8
Online ISBN: 978-3-540-68454-1
eBook Packages: Springer Book Archive