Re: DAML+OIL semantics

From: Jim Farrugia <jim@spatial.maine.edu>
Subject: DAML+OIL semantics
Date: Sun, 11 Aug 2002 12:58:41 -0400 (EDT)

> I have some questions about the semantics of DAML+OIL, and I'm wondering
> if this list is the appropriate place to post them.

Spot on.

> In a nutshell, the questions are:
> 
> 1. how to understand what it is that each kind of semantics 
> (axiomatic and model-theoretic) gives us, and why a developer would
> choose to use one kind of semantics rather than the other?

Well, a semantics for a representation language or logic should provide
meaning for the language.  Different kinds of semantics provide this
meaning in different ways.  

Model-theoretic semantics map the constructs of the language into
(hopefully) simple constructs (such as sets).  From this, generally,
notions of satisfaction and entailment are constructed.  Then properties of
entailment can be determined and used to build an implementation of the
language.

Proof-theoretic semantics provide rules for determining inference in the
language.  These rules can then either be directly implemented or used to
build an implementation of the language.  It is very unlikely that a useful
implementation can be directly taken from a proof theory unless the proof
theory was specially designed for this purpose.

An axiomatization (not axiomatic semantics) of a language is a collection
of formulae in some logic that implements inference in the language, or, in
the case of DAML+OIL, that implements inference in a translation of the
language.  If the target logic has implemented reasoners, the
axiomatization can be used in these reasoners to create a reasoner for the
language.  Again, this reasoner will usually be ineffective unless care is
taken to write the axiomatization in a manner that exploits the strengths
of the target logic reasoner.

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.
2/ Proof theories can point the way to effective reasoners.  It is often
   simple to turn a proof theory into a reasoner, especially if it is
   similar to other proof theories that have been turned into reasoners.
   However, the reasoner may not turn out to be effective.
3/ Axiomatizations can lead to trivial implementations of reasoners - just
   use a reasoner for the target logic.  However, the reasoner may not turn
   out to be effective.

If you read up about description logics you will see the differences
between model theories and proof theories designed for implementation.

> 2. how does each kind of semantics handle notions such as satisfaction, 
> truth, validity (of sentences and of inferences), logical consequence, and 
> logical equivalence?

[The following is heavily abstracted.  For a good introduction to how
this is handled in a model theory you could read the new model theory for
RDF.] 

Model theories are based directly on interpretations and truth
(satisfaction) in an interpretation.  From that they define validity as
being true in all interpretations and satisfiability as being true in some
interpretation.  Logical consequence is usually defined as the consequent
being true in every interpretation that makes the antecedant true.  Logical
equivalence is just two-way consequence.  Model theories are not concerned
with inferences.

Proof theories are based directly on the notion of (some form of)
inference.  There is no notion of truth in a proof theory.  Validity of a
sentence is defined as something that can be infered from an empty
antecedant.  Validity does not make sense with respect to inferences, as
inferences are just things that can be done in a proof theory.  Neither logical
consequence nor logical equivalent make sense in a proof theory, but 
often correspond most closely to inferrable from.

Axiomatizations use whatever the target logic uses, under the mapping
mapping into the target logic.


> 3. is an inference based on the axiomatic semantics valid if and only if
> the inference is valid using the model-theoretic semantics, and how can
> this be shown?

The general idea is to define a logic (or representation formalism) in
terms of a syntax and a model theory.  Then one shows that a proof theory
or axiomatization is sound (anything provable is an entailment) and/or
complete (any entailment is provable) with respect to the model theory.
There are many tools for doing this, some relatively easy and some
extraordinarily difficult.  It is also possible to have proof theories or
axiomatizations that are sound but not complete or complete but not sound
(or, perhaps, neither sound nor complete).

> 4. how does each kind of semantics handle the jump from symbols to the 
> state of affairs in the real world (or in the world of URIs) that the 
> symbols purport to describe?

Answer 1/ They don't.  How can they?  A semantics is just a formal system.  

Grounding of symbols has to be done in some other manner, perhaps through
sensors and effectors.

Answer 2/ Model theories are supposed to be simple formal systems, so
simple that the mapping from interpretations to the real world is trivial
(but not part of the semantics).

Answer 3/ Proof theories implement the way people do reasoning so whatever
people do to ground their symbols can be done in or as an adjunct to a
proof theory.

Which answer you prefer is up to you.

> I can elaborate on these questions if this email-list is the right
> place for such a discussion.
> 
> If it is, please let me know and chime in.
> 
> If it's not, please direct me to the appropriate place(s) or people.
> 
> Thank you,
> 
> Jim


Peter F. Patel-Schneider
Bell Labs Research

Received on Sunday, 11 August 2002 17:23:06 UTC