An extension of pointwise circumscription

AbstractIn this paper we generalize Lifschitz's pointwise circumscription ander the first-order framework. The generalized version has the ability for simultaneously minimizing several predicates at finitely many pinpoints in a pointwise manner. We show that if an anderlying first-order theory is almost existential, then the extended pointwise circumscription is complete with respect to minimal model semantics. Almost existential formulas are in the dual form of almost universal formulas, which was proposed by Lifschitz to investigate the satisfiability of circumscription. This completeness result is a generalization of the result by Kolaitis and Papadimitriou, who regarded the case of existential formulas. We also give a partial answer to the question for exponential growth of the size of first-order formulas equivalent to circumscription. Moreover we clarify that Lifschitz's pointwise circumscription is complete in a slightly wider class of positive formulas