Re: [RIFRAF] ho to proceed? Part I: Ontologization

> 1) First, I will try to get something towards ontologization out of the
> whole core discussion, and raise some open questions there.


We agreed that several people take over parts of the ontologization
according to the sections of the questionnaire [3].

   Supposedly, an overall ontology on what is a rule, condition, head,
body, etc. would be a starting point for axiomatizing the
discruiminators mentioned there.
Thus, for giving it a start, I concentrated to modeling conditions and
what is currently in the core properly for the moment.
   I picked up a rudimentary attempt by Sandro [1] and started to
additionally "OWLify" what I found in the last core version [2].
Find the result as an attachment.
If you think this approach makes sense, we could maybe further develop
this jointly using subversioning or similar versioning software...


Just to demonstrate why I think this is a valid starting point for
defining axioms concerning discriminators in the current RIFRAF,
and in which direction this could go let's look at the following
question/discriminator from [3]:

"1.2 Predicate Variables Permitted vs. Not Permitted
Does your language allow predicate variables? [...]"

This could be "axiomatized" somewhat as follows using the basic
ontology started now by stating (I use some F-Logic-style syntax here,
just to get to the point, hope it is readable enough):

=======================================================================
% Axiomatizing 1.2 in the rifraf ontology:

% PredVarNotPermitted is a subclass of Language
predVarNotPermitted::Language.


% Define an  auxiliary predicate to "collect" recursively
% all "subConditions":

forall C, C1. C[hasCondition -> C1] implies C[hasSubCondition -> C1]

forall C. C[hasCondition -> C1[hasSubCondition -> C2] implies
             C[hasSubCondition -> C2]


% Finally the rule which disallows variales for the
% predVarNotPermitted languages:

forall L, R,C,F.
( L:predVarNotPermitted and
    R[hasRecCondition->C:ComplexTerm[hasFunctor->F:Variable]]
)
implies
neg R[expressibleIn->L]
=======================================================================

   Main open issues are:

a) Well, this probably looks a lot like Sandro's attempts to make an
abstract syntax notation which is not surprising.

b) I came to some limits very quickly, e.g.
    How do I express that a parameter has at least one position or functor
    describing the argument-name. This can be done in OWL, but not in
    protege (without adding a new class). Likewise, I am unsure whether
    the 1.2 axiomatization above can be encoded in OWL properly.

c) Is this exercise useful or shall we wait until we have the core
     fixed before continuing?
     For instance: When we go further towards e.g. events, one has to ask
     him/herself for instance whether events are a subclass of "condition"
     or something different? How can I axiomatize in an extensible way
     that Core rule has no events in its body, etc.
     It seems to me that for expressing this, I need integrity constraints
     not expressible in OWL...

FWIW, I would like to discuss the general approach before continuing,
honestly.

best,
axel

1. http://lists.w3.org/Archives/Public/public-rif-wg/2006Oct/0093
2. http://www.w3.org/2005/rules/wg/wiki/CORE?action=recall&rev=14
3. http://www.w3.org/2002/09/wbs/38457/RAFQuestionnaire/

-- 
Dr. Axel Polleres
email: axel@polleres.net  url: http://www.polleres.net/