From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Sun, 11 Aug 2002 17:21:37 -0400

To: jim@spatial.maine.edu

Cc: www-rdf-logic@w3.org

Message-Id: <20020811172137F.pfps@research.bell-labs.com>

Date: Sun, 11 Aug 2002 17:21:37 -0400

To: jim@spatial.maine.edu

Cc: www-rdf-logic@w3.org

Message-Id: <20020811172137F.pfps@research.bell-labs.com>

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 ResearchReceived on Sunday, 11 August 2002 17:23:06 UTC

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