W3C home > Mailing lists > Public > www-rdf-logic@w3.org > August 2002

Re: DAML+OIL semantics

From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
Date: Mon, 19 Aug 2002 11:19:56 -0400
To: jim@spatial.maine.edu
Cc: www-rdf-logic@w3.org
Message-Id: <20020819111956L.pfps@research.bell-labs.com>

From: Jim Farrugia <jim@spatial.maine.edu>
Subject: Re: DAML+OIL semantics
Date: Tue, 13 Aug 2002 11:18:14 -0400 (EDT)

> Peter,
> 
> The longer one.
> 
> Thanks for your replies.
> 
> 
> Jim
> 
> 
> 
> JF:    > 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?
> 
> P P-S: The general idea is to define a logic (or representation formalism) 
>        in terms of a syntax and a model theory.  Then one shows that aproof 
>        theory or axiomatization is sound (anything provable is an entailment) 
>        and/or complete (any entailment is provable) with respect to the model 
>        theory.  
>        
> JF:    OK, let's see....
> 
> 
>        1) what is the right way to get at the question whether the DAML+OIL 
>        axiomatic semantics "gives us the same thing" as the DAML+OIL 
>        model-theoretic semantics?  Does it make sense to try to ask such
>        a question, or is it a case of apples and oranges?

This is a valid question.  To be more precise, the kind of question that
you can ask is, given the axiomatization, A, and two DAML+OIL KBs, K and Q,
whether 
	K entails Q in the model theory
iff
	K + A entails Q in the model theory of the logic underlying the
	axiomatization

One can also ask an equivalent question, namely whether 
	K entails Q in the model theory
iff
	Q can be derived from K + A in a sound and complete proof theory
	for the logic underlying the axiomatization

Unfortunately, the answer to this question is no.

>        On the one hand, the model-theoretic semantics says: "The semantics is 
>        specified via mappings from syntactic structures to constraints on 
>        semantic structures. ...  A semantic structure <AD,IC,IO,IR> is a 
>        model for the DAML+OIL ontology if the constraints resulting from the 
>        mappings from the ontology are true in the structure."

Well, the model theory does not actually have a notion of entailment built
it, but it is very easy to define:
	K entails Q iff any model for K is also a model for Q

>        On the other hand, the axiomatic semantics says: "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."

Well, intended meaning is, sort of by definition, a non-formal notion, so
it is very hard to be logicially equivalent to an intended meaning.  

>        These are the two notions I'm trying to harmonize.
> 
>        They both seem to be saying, "OK, let's first agree on the syntactic
>        constructions we are using." Then, ...

>        The model-theoretic semantics seems to say, "Any structure
>        in which the specified semantic constraints hold true has captured
>        the meaning of our language. In effect, we define the semantics 
>        associated with the syntactic elements of our language by creating
>        mappings from these syntactic elements to set-theoretical structures
>        and then saying that language statements (once they undergo the 
>        appropriate mapping and are considered as saying something about 
>        the set-theoretic structure) that result true in these
>        structures define the meaning of the syntactic constructs used
>        in the language statements."
>        
>        The axiomatic semantics seems to be saying, "We believe that our
>        axioms and any inferences you can draw from them are a faithful 
>        rendering of what we intend should be the meaning of our syntactic 
>        constructs."
> 
>        So, both kinds of semantics set up conditions that constrain the 
>        sanctioned meanings of the syntactic constructs. 

What they are both trying to get at is a formal way of
providing meaning for knowledge bases, either directly via semantic
mappings, or indirectly via an axiomatization in another logic that has its
own semantic mappings.  So, yes.

>        The model-theoretic account specifies meanings through a collection 
>        of mappings from syntactic constructs into a set-theoretic 
>        structure and associated satisfaction relations for that structure, 
>        declaring that any structure following these mappings and evaluating 
>        satisfaction in the specified way defines the semantics of the language.
> 
>        The axiomatic account seems more open ended in that it seems to say: 
>        (after we translate the language to a particular logic), if
>        the syntactic elements obey all the axioms we lay out, then the
>        semantics of the language is defined by what is claimed by these 
>        axioms and whatever can be inferred from these axioms.
> 
>        Is this account accurate/plausible?  How would you change it?

Well, the axiomatization depends on whatever semantics is given to the
target logic.  As the target is close to FOL, one could either use a model
theory for the target logic similar to the model theory for FOL or a proof
theory similar to a proof theory for FOL.

>        And the question remains: how we can know that the two formulations
>        "give us the same thing"?  If the axioms and inferences of the
>        axiomatic semantics hold true in the models of the model-theoretic
>        semantics? ???

This would not work.

First the axioms and inferences of the axiomatic semantics are not
true in the interpretations of the model thery, as the axiomatization uses
a different method for assigning truth to triples.  The model theory does
something like saying that a triple (P S O) is true whenever a formula
P(S,O) is true.  The axioimatization, instead, uses something like
holds(P,S,O).  Because of this, to make comparisons at this level requires
a transformation between the two kinds of interpretations. 

Second, the condition would not be sufficient, even if it was true, because
you also have to show that the inferences are also complete.


Your questions touch on many difficult issues with respect to logic, and
thus are difficult to answer completely in anything less than a long
paper.  I hope, however, that my replies are helpful.


peter
Received on Monday, 19 August 2002 11:21:21 UTC

This archive was generated by hypermail 2.3.1 : Wednesday, 2 March 2016 11:10:38 UTC