From: Hassan Aït-Kaci <hak@ilog.com>

Date: Fri, 09 Dec 2005 21:52:54 +0100

Message-ID: <4399EEA6.3010702@ilog.com>

To: Pascal Hitzler <hitzler@aifb.uni-karlsruhe.de>

CC: Jim Hendler <hendler@cs.umd.edu>, Enrico Franconi <franconi@inf.unibz.it>, Uli Sattler <Ulrike.Sattler@manchester.ac.uk>, public-rif-wg@w3.org

Date: Fri, 09 Dec 2005 21:52:54 +0100

Message-ID: <4399EEA6.3010702@ilog.com>

To: Pascal Hitzler <hitzler@aifb.uni-karlsruhe.de>

CC: Jim Hendler <hendler@cs.umd.edu>, Enrico Franconi <franconi@inf.unibz.it>, Uli Sattler <Ulrike.Sattler@manchester.ac.uk>, public-rif-wg@w3.org

Pascal Hitzler wrote: > Hassan, > > I very much apprechiate your point - the term "formal semantics" is easily interpreted in too narrow a sense. But let me just add (and emphasize, as I assume that you agree with me on this) that procedural semantics alone is not satisfactory for a semantic web context, as it usually binds a language to a specific engine, and is thus not in the spirit of interoperability and interchange. > > Best Regards, > > Pascal. Hi Pascal, I do not know what you mean by "procedural semantics". I was simply expressing the fact that one should not equate "formal semantics" with "model-theoretic semantics". SOS and Natural Semantics, that I cite as examples of "formal operational semantics", are based on syntax transformation rules. Computation or inference thereby expressed, amounts to normalization of forms (e.g., formulas, expressions, constraints, ...) into some canonical (or irreducible, or solved) form. Such an operational semantics is every bit as formal as model-theoretic denotational semantics, and IMHO is very intuitive and do not resort to positing existence of any fancy algebraic structures or domains to explain what is being expressed. In addition, proof- theoretic or normalization rules are directly executable - something that most model-theoretic semantics are not due to non-constructive existence of models. Correctness in rule-based semantics is not defined in terms of adequation between proofs and models, but amounts to etablishing that each rule preserves some formal property (whether syntactical or semantical). One must not confuse "implementation" (such as what you call a "rule engine") and the formal specification of a process formulated as a proof-theoretic system. For example, I can describe FO term unification with 5 simple non-deterministic equation transforming rules without presuming in any way what would be the most efficient way of implementing the specified process in any specific programming language. The correctness of this process means simply to show that all rules preserves all and only the solutions of the transformed equations. From these rules, I would thus be able to obtain a correct executable unification machine which would allow me to compare the results of several disctinct implementations of the same algorithm. The situation is the same for a RIF: if one can specifiy several rule-based semantics using a uniform proof-theoretic formalism (a la SOS, Natural Semantics, or any equivalent meta-formalism) and encode that in XML, RDF, or whatever fashionable such notation, which could both represent ontological data (i.e., classes and objects) as well as a single meta-rule normalization calculus, one will then have a RIF. Is this clearer? Cheers, -hak -- Hassan Aït-Kaci ILOG, Inc. - Product Division R&D tel/fax: +1 (604) 930-5603 - email: hak @ ilog . comReceived on Friday, 9 December 2005 20:56:23 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Tuesday, 2 June 2009 18:33:25 GMT
*