The complexity of predicate default logic over a countable domain
Lifschitz introduced the notion of defining extensions of predicate default theories not as absolute, but relative to a specified domain. We look specifically at default theories over a countable domain and show the set of default theories which possess an ω-extension is Σ21-complete. That the set is in Σ21 is shown by writing a nearly circumscriptive formula whose ω-models correspond to the ω-extensions of a given default theory; similarly, Σ21-hardness is established by a method for translating formulas into default theories in such a way that ω-models of the circumscriptive formula correspond to ω-extensions of the default theory. (That the set of circumscriptive formulas which have ω-models is Σ21-complete was established by Schlipf.)
"The Complexity of Predicate Default Logic over a Countable Domain", Annals of Pure and Applied Logic 120, 1-3 (April 2003), pp. 151-163.
Annals of Pure and Applied Logic