Folks, (01)
The issue of nonmonotonic reasoning is important for many practical
applications, and I'd like mention a version that I recommended in my
knowledge representation book. The method is based on "prioritized
defaults," as developed by Benjamin Grosof: (02)
http://www.mit.edu/~bgrosof/paps/rc20836.pdf (03)
For a brief overview, see my summary (copy below) from Section 6.4
of the KR book. Note that the basic axioms and the default axioms
use nothing beyond a classical first-order logic. However, the
priority mechanism uses two metalevel notations that go beyond FOL: (04)
1. A method of naming axioms, such as Mol, Cep, and Nau. (05)
2. A collection of metalevel assertions with the predicate "overrides"
that define a partial ordering of the default axioms. (06)
Grosof's approach is a version of default logic, in which there are
multiple defaults prioritized in a partial ordering. Whenever there
is a conflict (contradiction) between two or more defaults, the one
with the highest priority, as defined by the partial ordering, is
chosen. (07)
Although Grosof presented the approach as a version of nonmonotonic
logic, exactly the same computational techniques can be viewed as a
method of belief revision based on a partial ordering of classical
first-order theories: (08)
1. The most general theory T at the top of the partial ordering
is defined by the set of classical (i.e., non-default) axioms. (09)
2. By Grosof's definition, each of the defaults is consistent with
the theory T defined by the classical axioms and with each axiom
above it and below it in the partial ordering. (010)
3. Therefore, it is possible to convert the partial ordering of
defaults into a partial ordering of theories. The classical
axioms define T at the top, and the theory Tn at any node n
below the top is defined by the axioms of T and a conjunction
of all the default axioms from each node on the path from the
top to n. (011)
Note that each theory Tn in the partial ordering is purely classical,
and no metalevel notation is needed to express any axioms in Tn. (012)
With this interpretation, Grosof's technique can be viewed as a
method of belief revision that selects a path from a classical
base theory T to a more specialized classical theory Tn. Each
step on the path from T to Tn monotonically increases the number
of provable statements. Any sideways step from one path to
another, however, is a nonmonotonic move that blocks one or
more conclusions while enabling others. (013)
I do not claim that the method of prioritized defaults is the only
method of nonmonotonic reasoning, but I do claim the following: (014)
1. It's a useful, general method that should be considered. (015)
2. It can be used in conjunction with a classical base logic
such as CL. (016)
3. The notation for writing the base axioms and the default
axioms does not require any feature beyond classical logic. (017)
4. The metalevel features for naming axioms and stating the
levels of priority (sometimes called 'entrenchment') are used
during the nonmonotonic reasoning process, but they can all
be eliminated from the final classical theory that has been
selected as a result of that reasoning. (018)
5. It shows that this method of belief revision is just as
efficient as the equivalent method of nonmonotonic logic
-- because it can use exactly the same algorithms, but
reinterprets what the algorithms are doing. (019)
6. The semantics of the chosen theory requires nothing beyond
a conventional Tarski-style model, and the methods for
defining the defaults can be treated as heuristics that
are justified by empirical evidence from the subject matter. (020)
John Sowa
_____________________________________________________________________ (021)
Prioritized Defaults. Benjamin Grosof (1997) used metalanguage to
specify the priorities of different defaults. To illustrate the
technique, he adapted an example from Etherington and Reiter (1983)
about the shell-bearing properties of mollusks. The first two axioms,
which have no exceptions, say that every nautilus is a cephalopod,
and every cephalopod is a mollusk: (022)
* (Ax)(nautilus(x) -> cephalopod(x)). (023)
* (Ax)(cephalopod(x) -> mollusk(x)). (024)
By default, every mollusk is shell bearing; a cephalopod, however,
is usually not shell bearing; but a nautilus is shell bearing.
Grosof represented those defaults by named axioms: (025)
* Mol: (Ax)(mollusk(x) -> shellBearer(x)). (026)
* Cep: (Ax)(cephalopod(x) -> ~shellBearer(x)). (027)
* Nau: (Ax)(nautilus(x) -> shellBearer(x)). (028)
If any instance x happened to trigger the Cep axiom together with
the Mol or Nau axioms, a contradiction would arise. To resolve that
conflict, the next two metalevel statements assert that the Nau
axiom takes priority or overrides the Cep axiom, and the Cep axiom
overrides the Mol axiom: (029)
* overrides(Nau,Cep). (030)
* overrides(Cep,Mol). (031)
Whenever the condition parts of two or more named axioms happen to
be true for the same instance, the theorem prover checks which axioms
have priority. Then it ignores the axioms that are overridden. (032)
When all axioms are represented in a Horn-clause form (Prolog style),
Grosof proved that a partial ordering of defaults determines a unique,
noncontradictory solution for every instance. Given that Molly is
a mollusk, Sophie is a cephalopod, and Natalie is a Nautilus, these
axioms would predict that Molly and Natalie are shell bearing, but
Sophie is not. (033)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (034)
|