Circumscription is a non-monotonic logic created by John McCarthy to formalize the common sense assumption that things are as expected unless otherwise specified.
[1][2] Circumscription was later used by McCarthy in an attempt to solve the frame problem.
This minimization is similar to the closed-world assumption that what is not known to be true is false.
The problem considered by McCarthy was not that of finding a sequence of steps to reach the goal (the article on the missionaries and cannibals problem contains one such solution), but rather that of excluding conditions that are not explicitly stated.
On the other hand, the existence of this bridge is not excluded by the statement of the problem either.
That the bridge does not exist is a consequence of the implicit assumption that the statement of the problem contains everything that is relevant to its solution.
Explicitly stating that a bridge does not exist is not a solution to this problem, as there are many other exceptional conditions that should be excluded (such as the presence of a rope for fastening the cannibals, the presence of a larger boat nearby, etc.)
Circumscription was later used by McCarthy to formalize the implicit assumption of inertia: things do not change unless otherwise specified.
However, the solution proposed by McCarthy was later shown leading to wrong results in some cases, like in the Yale shooting problem scenario.
This lets us define models that do not assign variables to true unless necessary.
as a formula having exactly the above set of models; furthermore, one can also avoid giving a definition of
A propositional formula having exactly these two models is the following one: Intuitively, in circumscription a variable is assigned to true only if this is necessary.
The extension of circumscription with fixed and varying predicates is due to Vladimir Lifschitz.
In particular, two kind of variables can be considered: The difference is that the value of the varying conditions are simply assumed not to matter.
Formally, the extension of circumscription that incorporate varying and fixed variables is as follows, where
The solution to the frame problem proposed by McCarthy is based on circumscription with no fixed conditions.
In the propositional case, this solution can be described as follows: in addition to the formulae directly encoding what is known, one also define new variables representing changes in the values of the conditions; these new variables are then minimized.
For example, of the domain in which there is a door that is closed at time 0 and in which the action of opening the door is executed at time 2, what is explicitly known is represented by the two formulae: The frame problem shows in this example as the problem that
is not a consequence of the above formulae, while the door is supposed to stay closed until the action of opening it is performed.
to model changes and then minimizing them: As shown by the Yale shooting problem, this kind of solution does not work.
The original definition of circumscription proposed by McCarthy is about first-order logic.
is assigned to true on a minimal set of tuples of values.
This formula states that extension minimization has to be done: in order for a truth evaluation on
This idea can be formalized by minimizing a single predicate expressing the abnormality of situations.
In particular, every known fact is expressed in logic with the addition of a literal
Minimizing the extension of this predicate allows for reasoning under the implicit assumption that things are as expected (that is, they are not abnormal), and that this assumption is made only if possible (abnormality can be assumed false only if this is consistent with the facts.)
In the propositional case, pointwise and predicate circumscription coincide.
A model is minimal only if it is not possible to turn any such value from true to false while still satisfying the formula.
An earlier formulation of circumscription by McCarthy is based on minimizing the domain of first-order models, rather than the extension of predicates.
Theory curbing is a solution proposed by Thomas Eiter, Georg Gottlob, and Yuri Gurevich.