A new class of theories for which circumscription can be obtained via the predicate completion
Sukhamay Kundu · Journal of Experimental & Theoretical Artificial Intelligence · 1996
Computing circumscription of a first-order theory is difficult because it involves, in general, a second-order quantifier. It is therefore important to study the cases where the circumscription can be expressed as a first-order theory. Lifschitz and Rabinov have previously shown that the class of separable theories and the class of collapsible theories have this property. Here, we introduce a new class of theories δ, called finitary theories, for which the circumscription CIRC(δ,P,Q) is given by a first order theory δ ∪ δpc, where δpc is the set of predicate completion formulas for predicates in P defined in a suitable way. There are many finitary theories which are interesting and which do not belong to the class of separable or collapsible theories.