Bad News: • Circumscription axiom is second-order (quantifying over predicates). • When CIRC(KB;P) is not first-order definable ? no theorem prover. Good News: • Applicable to arbitrary first-order theories. • Sometimes CIRC(KB;P) is first-order definable. • Systematic procedures for computing CIRC(KB;P) sometimes.