Once again, there are other syntactic classes of KBs for which circumscription is first-order definable and can be systematically computed. Computing circumscripton for formulae that are solitary in Z. CIRC(N[Z] ? (E ? Z) ; P; Z) ? N[Z] ? (E ? Z) ? CIRC(N(E); P)where N has no positive occurrences of Z, and E has no occurrences of Z. E, P, and Z can be tuples of predicatesReturning to our ExampleE.g., KB= (block(x) ? ? ab(x) ? ontable(x)) ?  ?ontable(B1) ? block(B1) ? block(B2) ? B1 ? B2Task: Want to infer ontable(B2),  but currently, KB ?? ontable(B2) and KB ?? ? ontable(B2)Let’s see what happens if we compute CIRC(KB; ab; ontable) N[ontable] = ?ontable(B1) ? block(B1) ? block(B2) ? B1 ? B2  (E ? Z) = block(x) ? ? ab(x) ? ontable(x)CIRC(KB; ab; ontable) ? N[ontable] ? (E ? Z) ?  CIRC(( (? block(B1) ? ab(B1)) ? block(B1) ? block(B2) ? B1 ? B2); ab)  Hence CIRC(KB; ab; ontable) ? KB ? (ab(x) ? x=B1)

Computing Circumscription

Previous slide

Next slide

Back to first slide

View graphic version