Circumscription is first-order definable and can be systematically computed for formulae solitary in P. Recall, a clause is solitary in P if, whenever it contains a positive occurrence of P, it contains only one occurrence of P. Hence, we can say that a formula is solitary in P if it can be written in the following normal form N[P] ? (E ? P) N[P] is a formula containing no positive occurrences of P E is a formula containing no occurrences of P E ? P is an abbreviation for (?x.E(x) ? P(x)) CIRC(N[P] ? (E ? P) ; P) ? N[E] ? (E ? P) , where N[E] is N[P] with each occurrence of P replaced by E Observe: Circumscription gives the same result as predicate completion does in the special case of conjunctions of clauses solitary P, these reduce to (E ? P)
Computing Circumscription