SCAN

Computing Circumscription

Circumscription was proposed by John McCarthy as a logically simple and clear means to do default reasoning. As an example consider the database consisting of the single entry flies(Tweety). From this database you can of course prove that Tweety flies. But if you ask the query flies(Woodstock)? then the database either answers with `don't know' or it responds brutally with `no'. If you have evidence that your database is complete then the answer `no' is justified. But in this case you conclude -flies(Woodstock) from the fact that flies(Woodstock) is not provable from the database. Since predicate logic is only semi decidable, this is not a complete procedure. Moreover, there is no clear semantics that allows you to justify this step.

McCarthy's circumscription idea solves this problem on the semantic level. The idea is to axiomatize in a certain sense the information "this is all I know about a particular predicate P", i.e. I want consider only those interpretations for P where P(x) is true only for the absolutely minimum number of x necessary to satisfy the database. This minimization of the extension of predicate symbols is called circumscription. Unfortunately the formula which axiomatizes the minimized predicate is second-order.

In the simplest case it is as follows:

circ(F[P],P) = F[P] & all P* (F[P*] & (P* -> P)) -> (P -> P*)

F[P] is an arbitrary first-order formula containing the predicate P which is to be minimized. F[P*] is like F, but all occurrences of P replaced by P*. P* -> P is short for all x1,...,xn (P*(x1,...,xn) -> P(x1,...,xn)). You can also have a list of predicates to be minimized simultaneously. Then P* -> P stands for the conjunction of all these implications.

Consider our little database above: flies(Tweety). According to the definition of circumscription,

circ(flies(Tweety),flies) = flies(Tweety) & all flies* (flies*(Tweety) & (all x flies*(x) -> flies(x))) -> (all x flies(x) -> flies*(x)).

This calls for a quantifier elimination procedure. We have to eliminate the predicate flies*. If we do this with SCAN, we find as a result:

circ(flies(Tweety),flies) = flies(Tweety) & (all x flies(x) -> x = Tweety),

i.e. Tweety is the only thing that flies.

In an extended version of circumscription one can minimize certain predicates at the cost of certain other predicates which are allowed to vary. That means if P are the predicates to be minimized and Z are the predicates allowed to vary then circ(F[P,Z],P,Z) is a formula from which one might be able to prove additional positive facts about Z which are not provable from F[P,Z]. The circumscription formula for this version is

circ(F[P,Z],P,Z) = F[P,Z] & all P*,Z* (F[P*,Z*] & (P* -> P)) -> (P -> P*)

In the current implementation we realized this general version of circumscription by generating the circumscription formula according to the above schema and then applying SCAN to the second-order part.

Since the original circumscription formula is second-order, there are various attempts to compute first-order circumscription directly from the original formula. But this is possible only in restricted cases, not for general predicate logic formulae. We have not yet done a systematic comparison of our quantifier elimination based approach with the other methods. But with this implementation there is now a basis to start a more general investigation.

References