Abbreviations: P* ? P is an abbreviation for (?x.P*(x) ? P(x)) P* ? P is an abbreviation for (P* ? P) ? ? (P ? P*) P* ? P is an abbreviation for (P* ? P) ? (P ? P*) The axiom schema ?P*. ( KB(P*) ? (?x.P*(x) ? P(x)) ) ? (?x.P(x) ? P*(x)) can be rewritten as ?P*. KB(P*) ? ? (P* ? P) which can be rewritten as ? (?P*. KB(P*) ?(P* ? P)) Hence, CIRC(KB;P) ? KB(P) ? ? (?P*. KB(P*) ?(P* ? P))
Simplifying the Circumscription Axiom