Re: DAML+OIL semantics

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

> 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'?

Well, there are lots of interrelated notions having to do with whether one
thing follows from another.  Different people use different names for them.
So by ``entailment'' I mean the above relationship between models.  Logical
consequence can be used for this as well.

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

Well one might be able to prove, for example, that every formula follows
from every other formula.  This would be a rather useless logic, of course,
but if you could prove this, implementation would be rather easy.
It is more normal to prove that some proof theory is sound and complete
with respect to entailment and use the proof theory to drive
implementation.  

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

Yes.

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

Axiomatizations are somewhat similar to proof theories in that they talk
mostly about inference.  However, the mapping to the other logic, along
with the axiomatization, can be used to provide a sort of rough-and-ready
meaning for each construct, which is what is being alluded to here.

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

Yes, sort of.  For example, the DAML+OIL axiomatization maps properties
into a holds predicate.  The behaviour of this holds predicate, including
the axioms about it, in the model theory of FOL can be used to characterize
a meaning for properties.

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

Logical equivalence can be considered to be ``can be derived from one
another'', so, yes, axiomatizations and proof theory can be considered to
provide a sort of logical equivalence.

> I'll stop this set of questions here, and continue later with others.
> 
> Thanks very much for your detailed answers.
> 
> Jim

[...]

In general, semantics of logics is trying to formalize a collection of
notions about logics that are often ill-understood by non-logicians.  It is
thus not surprising that there are many ways of taking these notions and
mapping them into the formal notions of the semantics.

peter

Received on Monday, 12 August 2002 06:32:16 UTC