[ontoiop-forum] OntoIOp teleconference (n.63): Wed 2014.09.10

[John F Sowa]

Till,

A few comments:

> so Cyc also uses the terms generalization and specialisation?

No, but those terms cover Cyc as well as many other systems.

JFS
>> every nonmon proof corresponds to a walk in a lattice of theories.

TM
> Yes, but the important point is that languages like RIF specify in
> detail how this walk looks. And then the question is how to abstract
> these specifications of such walks to a general notion of nonmonotonic
> logic.

I agree.  The methods of nonmon logic -- especially NAF -- are very
useful methods of inference.  Anything useful is worth keeping.

But every version of nonmon logic has a different kind of semantics
for justifying its proofs.  The advantage of the lattice of theories
is that it provides a single framework for interpreting both classical
and nonmonotonic inference rules.

A classical proof starts at a single node in the lattice of theories,
and it stays at that node throughout the proof.

A nonmonotonic proof takes a walk through the lattice from one
classical theory to another.  The final theory is purely classical,
and the axioms of that theory are sufficient to carry out the proof
by purely classical methods.

I'm not suggesting that we get rid of the nonmon inference rules.
But what I am suggesting is that we interpret those rules as
guides for a walk through a lattice of purely classical theories.

The advantage of this method is that we only need one model theory
for specifying the semantics of both classical and nonmonotonic logics.

John