Re: DAML+OIL semantics

Peter,

Please see further comments and questions below,

which end with a line of ############################################

Thanks,

Jim


On Sun, 11 Aug 2002, Peter F. Patel-Schneider wrote:

> 
> 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.  

So far, so good.
 
> 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.


OK, with three questions for this part. 

When you say 'entailment' do you mean what others (e.g., Ebbinghaus, 
Flum, and Thomas, 2nd ed., 1994) mean by 'consequence' (p. 33, 34), 
where they say that a formula X is a consequence of a set
of formulas Y iff every interpretation that is a model of the set of
formulas Y is also a model of the formula X?

Isn't this notion the same as what you refer to below as 'logical
consequence'?

I'm not sure I understand your last sentence above about building
an implementation of the language. Can you sketch out how 
properties of entailment enable this is done?


> 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.


So, given that a semantics for a representation language should provide
meaning for that language, does it make sense to say that the meaning
a proof-theoretic semantics provides for a languages is just the 
set of rules that govern inference in the language?

By 'proof-theoretic semantics' are you talking about what DAML+OIL
calls 'axiomatic semantics'?  It doesn't seem so, since the
presentation of the axiomatic semantics for DAML+OIL says:


	This document provides an axiomatization for the Resource 
	Description Framework (RDF), RDF Schema (RDF-S), and DAML+OIL 
	by specifying a mapping of a set of descriptions in any one 
	of these languages into a logical theory expressed in 
	first-order predicate calculus. 

	The basic claim of this paper is that the logical theory 
	produced by the mapping specified herein of a set of such 
	descriptions is logically equivalent to the intended meaning 
	of that set of descriptions.

(http://www.ksl.stanford.edu/people/dlm/daml-semantics/daml+oil-axioms-october2001.htm)

These remarks seem to be claiming more for this axiomatic semantics 
than what you say a proof-theoretic semantics provides.

In particular, the above statement suggests that the axiomatic semantics
(the logical theory produced by the mapping) is trying to capture 
the _intended meaning_ of descriptions in RDF/S and DAML+OIL.
Such a claim seems to go over and above providing rules for determining 
inference in the language. ??

Further, given what you say below about logical equivalence, 
I don't see how/why it makes sense to say, as is done in the 
basic claim quoted above, that the logical theory produced 
by the mapping can be logically equivalent to an intended meaning. ??

If the axiomatic semantics doesn't use the model-theoretic
notions of truth and interpretation, then (again, considering
the characterization you give below of logical equivalence)
in what way is it proper to talk about the logical equivalence 
of a logical theory with something else?  And could this something
else ever be an intended interpretation?


I'll stop this set of questions here, and continue later with others.

Thanks very much for your detailed answers.

Jim

##############################################################################
 
> 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 22:15:29 UTC