Re: DAML+OIL semantics

On August 13, Peter F. Patel-Schneider writes:
> 
> From: Jim Farrugia <jim@spatial.maine.edu>
> Subject: Re: DAML+OIL semantics
> Date: Tue, 13 Aug 2002 10:41:47 -0400 (EDT)
> 
> > Peter,
> > 
> > I'm breaking up my questions into two short ones and one longer one.
> > 
> > Here's the first short one.
> > 
> > Jim
> > 
> > 
> > 
> > P P-S: So there are several reasons one would choose one semantics over 
> > another:
> > 
> >        1/ Model theories tend to be smaller and simpler, and thus easier to
> >        understand.  They are more declarative than proof theories or
> >        axiomatizations.  However, model theories generally are not 
> >        related to implementations of reasoners.
> > 
> > JF:    How in general to get from a model-theoretic semantics to an
> >        implementation with a reasoner? (Maybe I'll find this in the DL
> >        literature you refer me to below?)
> 
> There is lots of DL literature about this, but I don't know if there is a
> single reference that brings it to the fore.
> 
> Anyway, the general method is to design a proof system for the logic, show
> that it is sound and complete with respect to the model theory, and then
> implement the proof system.  This only results in an effective reasoner if
> the proof system is amenable to optimization.  Currently the tableaux
> calculus is the proof system of choice for this.
> 
> Showing that the reasoner implements the proof system can be difficult if
> the optimizations are complex.  Many avenues have been utilized here,
> including using results from other areas.

I would just like to add that whenever an algorithm/specification is
implemented, there is a likelihood of errors being introduced. The
more highly tuned/optimised the implementation, the greater this
likelihood. Unfortunately, proving the formal correctness of various
optimisations is difficult and time consuming. Moreover, the proofs
may be so large and complex as to be themselves subject to possible
errors. These kinds of problem are, of course, the subject of a great
deal of research in their own right.

In spite of these difficulties, I believe that it is still worthwhile
to start with a well specified algorithm in whose correctness we have
good reason to believe, even if some compromises are made at the
implementation stage. Moreover, the process of designing the algorithm
and proving its correctness often gives important insights into the
kinds of input that might be difficult to deal with and against which
any implementation should be tested.

The alternative approach, apparently favoured by some, is to implement
software according to their intuition as to how to solve the problem
at hand, testing and tuning as they go until the result appears to
perform satisfactorily.  Of course it is very difficult to be sure
exactly what this kind of software is implementing or how it will
behave with any inputs other than those against which it has been
explicitly tested.  I know from experience that intuitions about
reasoning algorithms are very often mistaken. Moreover, the kinds of
input that may cause problems are, almost by definition, just those
which intuition failed to consider and against which the
implementation will not be tested.

Regards, Ian





> 
> Peter F. Patel-Schneider
> Bell Labs Research

Received on Wednesday, 14 August 2002 06:02:09 UTC