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

Received on Saturday, 9 February 2008 17:12:17 UTC