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 secondorder.
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 firstorder 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 secondorder part.
Since the original circumscription formula is secondorder, there are various attempts
to compute firstorder 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.
SCAN Home
Forms:
Basic Form 
Correspondences Form 
Circumscription Form 
Help
Documentation:
Theory 
Computing Correspondences 
Computing Circumscription 
The System 
Conventions 
Syntax 
Literature
Maintained by
schmidt@cs.man.ac.uk.
Last modified: 05 Aug 13