Re: DAML+OIL semantics

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.

Peter F. Patel-Schneider
Bell Labs Research

Received on Tuesday, 13 August 2002 10:57:50 UTC