RE: different kinds of semantics

What about type checking in programming languages and databases?
How could this be included (if at all) in the framework below.

I know you have some papers comparing and contrasting type checking
with model theory and Alex Borgida also has done some work on the same.

Would be great to hear your thoughts on this issue.

---Vipul

> -----Original Message-----
> From: public-owl-wg-request@w3.org 
> [mailto:public-owl-wg-request@w3.org] On Behalf Of Peter F. 
> Patel-Schneider
> Sent: Saturday, February 09, 2008 12:08 PM
> To: public-owl-wg@w3.org
> Subject: different kinds of semantics
> 
> 
> Here is my take on various ways that one can specify semantics for a
> representation or modelling formalism.  This is a very short 
> high-level
> overview, without many specifics, but I think that it shows off the
> differences between the various kinds of semantics.  Note that I have
> only specified semantics for monotonic formalisms.
> 
> A/ Model-theoretic, e.g., most DL model theories
>       I. Horrocks, O. Kutz, and U. Sattler. The Even More Irresistible
>       SROIQ. KR2006. 
>       http://www.cs.man.ac.uk/~sattler/publications/KR-06-SROIQ.pdf 
> 
>    1/ Simple, generally set-theoretic, formal constructs
>       (interpretations) provide the grounding for the formalism.
>    2/ Interpretations are models of syntactic constructs when they
>       satisfy the formal semantic conditions provided for the
>       constructs.
>    3/ A formula is a consequence of a KB when every model of the KB is
>       also a model of the formula.  
> 
>    NB: If there is only one, finite model (or a single, 
> finite canonical
>        model) for a KB then this is just like the old method used to
>        provide semantics for RDF (ref?) and also like some 
> methods used
>        to provide semantics for databases and XML.
> 
> B/ Proof theoretic, e.g., FOL proof theories and DL proof theories
>       Martin Hofmann.  Proof-Theoretic Approach to
>       Description-Logic. LICS 2005.
>       http://www.tcs.informatik.uni-muenchen.de/~mhofmann/DL.pdf
> 
>    1/ Syntactic transformations (the proof theory) provide the basic
>       inferences of the formalism. 
>    2/ A formula is a consequence of a KB if a sequence of basic
>       inferences starting at the KB can produce the formula.
> 
> C/ Operational, e.g., Prolog specification as an abstract machine
> 
>    1/ A formula is a consequence of a KB if a particular algorithm (or
>       even a particular program) says that it is.
> 
>    This differs from the proof-theoretic approach in that a 
> proof theory
>    doesn't provide a fully specified algorithm.  In many 
> cases the proof
>    theory can easily be turned into a possibly non-deterministic
>    algorithm, but this might not always be the case.
> 
> D/ Informal, e.g., OWL Reference
>       Mike Dean and Guus Schreiber.  OWL Web Ontology Language
>       Reference. 2004. http://www.w3.org/TR/owl-ref/
> 
>    1/ Natural language (usually English) text describes the meaning of
>       the syntactic constructs of the formalism (without reference to
>       any of the above formal methods of providing semantics).
> 
> The next two methods define meaning based on meaning in some other,
> target, semantics. 
> 
> E/ Transformational, e.g., DL transforms into FOL
>       Ullrich Hustadt, Boris Motik, and Ulrike Sattler. Reducing SHIQ-
>       Description Logic to Disjunctive Datalog Programs.  KR2004.
>       
> http://web.comlab.ox.ac.uk/oucl/work/boris.motik/publications/
> hms04reducing.pdf
> 
>    1/ A formal mapping from the syntactic constructs into another
>       (hopefully simpler) formalism provides basic meaning.
>    2/ A formula is a consequence of a KB if the mapping of the formula
>       is a consequence of the mapping of the KB in the target
>       formalism. 
> 
> F/ Axiomatic, e.g., DAML+OIL axiomatic semantics
>       Richard Fikes and Deborah McGuinness.  An Axiomatic Semantics
>       for RDF, RDF-S, and DAML+OIL (March 2001).  W3C Note 18 December
>       2001.  http://www.w3.org/TR/daml+oil-axioms
> 
>    0/ If necessary, the formalism is transformed into another.
>    1/ A theory, in the form of a set of axioms in the (target)
>       formalism, provides (the bulk of) the meaning of 
> constructs in the
>       formalism. 
>    2/ A formula is a consequence of a KB if it is a consequence of the
>       KB plus the theory in the (target) formalism.
> 
> 
> Here are instantiations of the above for propositional logic. 
>   I'm not
> claiming that all of these are reasonable for propositional logic, but
> they should work OK. 
> 
> A/ Model-theoretic semantics
>    An interpretation is a total mapping from propositional letters to
>    true or false.  An interpretation is a model of a propositional
>    letter iff it maps the propositional letter to true.  An
>    interpretation is a model of a negation iff it is not a 
> model of the
>    negated formula.  An interpretation is a model of a conjunction
>    (disjunction) iff it is a model of both conjuncts (either 
> disjunct).
> 
> B/ Proof-theoretic semantics
>    From p infer p v q; from p ^ q infer p; from ~~p infer p; 
> from p v q
>    and ~p infer q; from p v q and p v ~q infer p; from p and 
> q infer p ^
>    q; ...
> 
> C/ Operational
>    Negate the proposed consequence, add it to the KB, and run 
> DPLL (with
>    some particular heuristic) to check for unsatisfiability.
> 
> D/ Informal
>    Propositional letters are either true or false; a negation 
> is true if
>    the negated formula is false; a conjunction is true if 
> both conjuncts
>    are true; a disjunction is true if either conjunct is true.  A
>    formula follows from another if it is true whenever the other is.
> 
> E/ Transformational
>    Define a mapping M from propositional letters to 0-ary predicates.
>    Transform a propositional formula into a FOL formula by replacing
>    propositional letters (l) with M(l)(), propositional negation with
>    FOL negation, and propositional conjunction (disjunction) with FOL
>    conjunction (disjunction).
> 
> F/ Axiomatic
>    Define a mapping M from propositional letters to constants.
>    Extend M to propositional formulae as follows:
>       M(~a) = Not(M(a))  where Not is a unary function symbol
>       M(a^b) = And(M(a),M(b)) where And is a binary function symbol
>       M(avb) = Or(M(a),M(b)) where Or is a binary function symbol
>    The transformation of a propositional formula a is then True(M(a))
>    where True is a unary prediate.
>    The theory is then
>       Ax ( x=TRUE v x=FALSE )
>       Not(TRUE) = FALSE       Not(FALSE) = TRUE
>       And(TRUE,TRUE) = TRUE   And(TRUE,FALSE) = FALSE ...
>       Or(FALSE,FALSE) = FALSE Or(TRUE,FALSE) = TRUE   ...
>       True(TRUE)      ~True(FALSE)
> 
> Peter F. Patel-Schneider
> Bell Labs Research
>  
> 
> 

The information transmitted in this electronic communication is intended only
for the person or entity to whom it is addressed and may contain confidential
and/or privileged material. Any review, retransmission, dissemination or other
use of or taking of any action in reliance upon this information by persons or
entities other than the intended recipient is prohibited. If you received this
information in error, please contact the Compliance HelpLine at 800-856-1983 and
properly dispose of this information.

Received on Saturday, 9 February 2008 17:36:08 UTC