Phokion G. Kolaitis, Christos H. Papadimitriou
We explore the effects of a circumscribing first-order formulae from a computational standpoint. First, extending work of V. Lifschitz, we show that the circumscription of any existential first-order formula is equivalent to a first-order formula. After this, we establish that a set of universal Horn clauses has a first-order circumscription if and only if it is bounded (when considered as a logic program); thus it is undecidable to tell whether such formulae have first-order circumscription. Finally, we show that there are first-order formulae whose circumscription has a coNP-complete model-checking problem.