Re: DAML+OIL semantics

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

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

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

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

Received on Tuesday, 13 August 2002 11:25:50 UTC