# zbMATH — the first resource for mathematics

An efficient method for eliminating varying predicates from a circumscription. (English) Zbl 0762.03013
Summary: Circumscription appears to be the most powerful and well-studied technique used in formalizing common-sense reasoning. The general form of predicate circumscription allows for fixed and varying (floating) predicates. We show that the inference problem under this form of circumscription is efficiently reducible to inferencing under circumscription without varying predicates. In fact, we transform this problem even into circumscription without fixed and varying predicates, that is where all predicates are minimized. Thus any theorem prover or algorithm for inferencing under circumscription without fixed and varying predicates is able to handle inferencing under the general form of predicate circumscription. As a consequence, algorithms that compute circumscription for an inference task can be simplified.

##### MSC:
 03B80 Other applications of logic 68T27 Logic in artificial intelligence 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
##### Keywords:
formalization of common-sense reasoning
Full Text:
##### References:
 [1] Bossu, G.; Siegel, P., Saturation, nonmonotonic reasoning and the closed world assumption, Artif. intell., 25, 13-63, (1985) · Zbl 0569.68078 [2] de Kleer, J.; Konolige, K., Eliminating the fixed predicates from a circumscription, Artif. intell., 39, 391-398, (1989) · Zbl 0672.03013 [3] Etherington, D.W., () [4] Etherington, D.W.; Mercer, R.E.; Reiter, R., On the adequacy of predicate circumscription for closed world reasoning, Comput. intell., 1, 11-15, (1985) [5] Gelfond, M.; Przymusinska, H., Negation as failure: careful closure procedure, Artif. intell., 30, 273-287, (1986) · Zbl 0635.68119 [6] Gelfond, M.; Przymusinska, H.; Przymusinski, T., On the relationship between circumscription and negation as failure, Artif. intell., 38, 75-94, (1989) · Zbl 0663.68097 [7] Ginsberg, M.L., A circumscriptive theorem prover, Artif. intell., 39, 209-230, (1989) · Zbl 0677.68096 [8] Hintikka, J., Reductions in the theory of types, Acta philos. fenn., 8, 61-151, (1955) · Zbl 0067.00201 [9] Lifschitz, V., Closed-world databases and circumscription, Artif. intell., 27, 229-235, (1985) · Zbl 0596.68062 [10] Lifschitz, V., Computing circumscription, (), 121-127 [11] Lifschitz, V., Pointwise circumscription, (), 406-410 [12] McCarthy, J., Circumscriptionâ€”a form of non-monotonic reasoning, Artif. intell., 13, 27-39, (1980) · Zbl 0435.68073 [13] McCarthy, J., Applications of circumscription to formalizing common-sense knowledge, Artif. intell., 28, 89-116, (1986) [14] Minker, J., On indefinite data bases and the closed world assumption, (), 292-308 [15] Przymusinski, T., An algorithm to compute circumscription, Artif. intell., 38, 49-73, (1989) · Zbl 0663.68098 [16] Reiter, R., On closed-world databases, (), 55-76 [17] Schlipf, J.S., Decidability and definability with circumscription, Ann. pure appl. logic, 35, 173-191, (1987) · Zbl 0625.03017 [18] van Benthem, J.; Doets, K., Higher order logic, (), 275-329, Chapter I.4 · Zbl 0875.03036 [19] Yahya, A.; Henschen, L., Deduction in non-Horn databases, J. autom. reasoning, 1, 2, 141-160, (1985) · Zbl 0614.68072 [20] Yuan, L.Y.; Wang, C.H., On reducing parallel circumscription, (), 460-464
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.