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

Date: Sat, 09 Feb 2008 12:08:29 -0500 (EST)

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

To: public-owl-wg@w3.org

Date: Sat, 09 Feb 2008 12:08:29 -0500 (EST)

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

To: public-owl-wg@w3.org

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 ResearchReceived on Saturday, 9 February 2008 17:12:17 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Saturday, 9 February 2008 17:12:18 GMT
*