Re: RIF vs Rule Language

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 . com

Received on Friday, 9 December 2005 20:56:23 UTC