# Different Kinds Of Semantics

Very useful explanation by Peter F. Patel-Schneider in the email below

Also, see Michael Schneider's discussion

```
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)

```