Some translation rules between some KRL model structures

Dr Ph. MARTIN

This document mixes HTML and FL (a KRL, i.e., a Knowledge Representation Language; it is here used in the preformatted text parts). It is an input+backup+presentation file for the Multi-Source Ontology (MSO). The MSO  i) aligns and extends several ontologies, and  ii) can be extended by Web users via the shared KB server WebKB-2 and its shared KB (knowledge base) editing protocols.
In this document, for supertype links, "/^" is used instead of the more common "<" symbol.
Similarly, for subtype links, "\." is used instead of the more common ">" symbol.

The ontology in this document is original. Some content is added to it from time to time.
It is part of a set of complementary "ontologies on formal languages":

The goals, underlying ideas, conventions and content of these ontologies are explained and illustrated in this article.


Table of contents
    1.  Between a property AE and an RDF reified statement
    2.  Between frames and conjunctions of binary relations from a same source
    3.  Between binary relations and non-binary ones
    4.  Between a property AE and an RDF reified statement


In each rule below, ":-" means "<=" and
the AE in bold font is the AEs (partially) defined by the rule.
Each r_descr relation relates a Descr_content (thing) to an AE.


1.  Between a property AE and an RDF reified statement

//Note: in FL, by default, variables prefixed by "%" are universally quantified
//  in their minimal context (e.g., a rule if they are in a rule)


[%prop /^^ Property  r_op: %op,
                     r_args: .[(%propSource  r_descr of: %describedPropSource)
                               (%propDest    r_descr of: %describedPropDest) ]
<=> [%prop  rdf#predicate: %op,  rdf#subject: %describedPropSource,
                                 rdf#object:  %describedPropDest ];

/* In RIF-BLD/RIF-PS:

  Forall ?prop  ?op   ?propSource ?describedPropSource  ?propDest ?describedPropDest  (
    ?prop[rdf:type Property   r_op->?op   r_args->List(?propSource ?propDest)]
    :- And (?prop [rdf:predicate->?op  rdf:subject->?describedPropSource
                                         rdf:object->?describedPropDest ] 
            ?describedPropSource[r_descr->?propSource]
            ?describedlPropDest[r_descr->?propDest] ) )

  Forall ?prop  ?op   ?propSource ?describedPropSource  ?propDest ?describedPropDest  (
    ?prop [rdf:predicate->?op  rdf:subject->?describedPropSource
                                 rdf:object->?describedPropDest ]
    :- And( ?prop[rdf:type Property  r_op->?op  r_args->List(?propSource ?propDest)]
            ?describedPropSource[r_descr->?propSource]
            ?describedlPropDest[r_descr->?propDest] ) )
*/


2.  Between frames and conjunctions of binary relations from a same source

The next rule relates the structures of two AEs (%c and %f) that are description instruments of something that is both a Thing_that_can_be_represented_via_binary-relations_from_a_same_source and a Thing_that_can_be_represented_via_a_frame. By default, in KRLO, these two types are related by an equivalence relation: see this Figure 4.2 of this article.
However, as explained in Section 3 of te same article, if the represented knowledge has more expressiveness than OWL-RL and RIF-BLD, this equivalence is not (always) true. Hence, to get the translation results she wants, i.e., for the next rule to apply only to certain types of frames and certain types of conjunctions of binary relations from a same source, the end-user can modify this equivalence relation by specializing its source type or destination type, hence restricting them. She can also remove this equivalence or keep it and have more complete results even if they may not always be correct.
Note: alone, the next rule is not sufficient to correctly handle quantifiers around the conjunction or the use of cardinality restrictions within the frame. This is handled by other rules.

And{[%relSource = %f_head]
    [%halfProperties  r_half-property-item_matching_this_binary-relation: %binRel]
    [%binaryRelations r_binary-relation_item_matching_this_half-property: %halfProperty] }
<= [%t /^^ Thing_that_can_be_represented_via_binary-relations_from_a_same_source
           Thing_that_can_be_represented_via_a_frame,
       r_descr_instrument: (%c /^^ Conjunction_of_binary-relations_from_a_same_source,
                               r_args: (%binaryRelations  pred#list-contains:
                                           (%binRel r_1st_arg: %relSource) ) )
       r_descr_instrument: (%f /^^ Frame_as_non-token-phrase,  r_op: %f_head, 
                               r_args: (%halfProperties pred#list-contains: %halfProperty) ) ];

//With the following definitions:
  Thing_that_can_be_represented_via_a_frame 
    <=> Thing_that_can_be_represented_via_binary-relations_from_a_same_source;

  r_half-property-item_matching_this_binary-relation ~[?halfProperties, ?binRel]
     := [?halfProperties  pred:list-contains:
            (a thing ?halfProperty  r_op: (an Operator ?relType  r_op of: ?binRel),
                                    r_1st_arg: (a Relation_node ?relDest  r_2nd_arg of: ?binRel) ) ];
  r_binary-relation_item_matching_this_half-property ~[?binaryRelations, ?halfProperty]
     := [?binaryRelations  pred:list-contains:
            (a thing ?binRel  r_op: (an Operator ?relType  r_op of: ?halfProperty),
                              r_2ng_arg: (a Relation_node ?relDest  r_1st_arg of: ?halfProperty) ) ];
  [%at  r_1st_arg: %arg1]  <=>  [%at  r_args: List(%arg1 | %l)];
  [%at  r_2nd_arg: %arg2]  <=>  [%at  r_args: List(%arg1 %arg2 | %l)];


/* In RIF-BLD/RIF-PS:
  Forall ?t  ?c  ?binaryRelations  ?binRel    ?f  ?f_head  ?halfProperties  ?halfProperty  (
    And( ?relSource = ?f_head
         r_half-property-item_matching_this_binary-relation(?halfProperties ?binRel)
         r_binary-relation_item_matching_this_half-property(?binaryRelations ?halfProperty) )
    :- And( ?t[rdf:type->Thing_that_can_be_represented_via_binary-relations_from_a_same_source
               rdf:type->Thing_that_can_be_represented_via_a_frame
               r_descr_instrument->?c    r_descr_instrument->?f ]    
            ?c[rdf:type->Conjunction_of_binary-relations_from_a_same_source
               r_args->?binaryRelations ]  
            ?f[rdf:type->Frame_as_non-token-phrase    r_op->?f_head
                                                      r_args->?halfProperties ]
            External(pred:list-contains(?binaryRelations  ?binRel))
            ?binRel[r_1st_arg->?relSource]
            External(pred:list-contains(?halfProperties  ?halfProperty))  ) )
  
  
  //With the following definitions:
    Forall ?t (
      ?t[rdf:type->Thing_that_can_be_represented_via_a_frame]
       :- ?t[rdf:type->Thing_that_can_be_represented_via_binary-relations_from_a_same_source] )
    Forall ?t (
      ?t[rdf:type->Thing_that_can_be_represented_via_binary-relations_from_a_same_source]
       :- ?t[rdf:type->Thing_that_can_be_represented_via_a_frame] )
  
    Forall ?halfProperties  ?halfProperty   ?binRel  ?relType  ?relDest  (
      r_half-property-item_matching_this_binary-relation(?halfProperties ?binRel)
      :- And( External(pred:list-contains(?halfProperties  ?halfProperty))
              ?halfProperty[r_op->?relType    r_1st_arg->?relDest]
              ?binRel[r_op->?relType    r_2nd_arg->?relDest] )  )
  
    Forall ?binaryRelations  ?halfProperty  ?binRel  ?relType  ?relDest  (
      r_binary-relation_item_matching_this_half-property(?binaryRelations ?halfProperty)
      :- And( External(pred:list-contains(?binaryRelations  ?binRel)) 
              ?binRel[r_op->?relType    r_2nd_arg->?relDest] 
              ?halfProperty[r_op->?relType    r_1st_arg->?relDest] )  )
  
    Forall ?at  ?arg1 ?l ( ?at[r_1st_arg->?arg1]
      :-  ?at[r_args->List(?arg1 | ?l) ]  )
  
    Forall ?at  ?arg1 ?arg2 ?l ( ?at[r_2nd_arg->?arg2]
      :-  ?at[r_args->List(?arg1 ?arg2 | ?l) ]  )
*/


3.  Between binary relations and non-binary ones

The next implication relates the structures of two AEs that are description instruments of something that is both a Thing_that_can_be_represented_via_a_non-binary_relation and a Thing_that_can_be_represented_via_a_binary_relation.
By default, in KRLO, these two types are related by an equivalence relation (the next rule can be used for translations in both directions).

And{ [%binRelArg1 = %nbrArg1] [%binRelArg2 = %nbrArgsExcept1st] }
 <= [%t /^^ Thing_that_can_be_represented_via_a_non-binary_relation
            Thing_that_can_be_represented_via_a_binary_relation,
        r_descr_instrument: (%nonBinRel /^^ Non-binary_relation,
                                        r_args: List(%nbrArg1 | %nbrArgsExcept1st) ),
        r_descr_instrument: (%binRel /^^ Binary_relation,
                                     r_1st_arg: %binRelArg1, r_2nd_arg: %binRelArg2 ) ];

//With the following definitions:
  Thing_that_can_be_represented_via_a_non-binary_relation
    has_descr_instrument<=: a Non-binary_relation, //actually "=:", not just "<=:" but "=: a ..."
    <=> (Thing_that_can_be_represented_via_a_binary_relation,       // cannot be translated to RIF-BLD
          has_descr_instrument<=: a Binary_relation );              // without skolem functions


/* In RIF-BLD/RIF-PS:

Forall ?t ?binRel  ?binRelArg1  ?binRelArg2     ?nonBinRel  ?nbrArg1  ?nbrArgsExcept1st  (
  And ( ?binRelArg1 = ?nbrArg1      ?binRelArg2 = ?nbrArgsExcept1st )
  :-  And( ?t [rdf:type->Thing_that_can_be_represented_via_a_non-binary_relation
               rdf:type->Thing_that_can_be_represented_via_a_binary_relation
               r_descr_instrument->?nonBinRel     r_descr_instrument->?binRel ]
           ?binRel[rdf:type->Binary_relation  r_1st_arg->?binRelArg1 
                                              r_2nd_arg->?binRelArg2] 
           ?nonBinRel[rdf:type->Non-binary_relation 
                      r_args->List(?nbrArg1 | ?nbrArgsExcept1st) ] ) )

//With the following definitions:

  Forall ?t ?nbr (
  ?t[rdf:type->Thing_that_can_be_represented_via_a_non-binary_relation]
   :-  And ( ?t[has_descr_instrument->?nbr]  ?nbr[rdf:type->Non-binary_relation] ) )
  
  Forall ?t ?br (
    ?t[rdf:type->Thing_that_can_be_represented_via_a_binary_relation]
     :-  And ( ?t[has_descr_instrument->?nbr]  ?br[rdf:type->Binary_relation] ) )

  Forall ?t (
    ?t[rdf:type->Thing_that_can_be_represented_via_a_binary_relation]
     :- ?t[rdf:type->Thing_that_can_be_represented_via_a_non-binary_relation] )

*/


4.  Between a function and a functional relation

And{ [%fctArgs = %fRelArg1] [%fctResult = %fRelArgsExcept1st] }
 <= [%t /^^ Thing_that_can_be_represented_via_a_functional_relation
           Thing_that_can_be_represented_via_a_function,
        r_descr_instrument: (%fRel /^^ Functional_relation,   r_op: %fRelType,
                                   r_args: List(%fRelArg1 | %fRelArgsExcept1st) ),
        r_descr_instrument: (%fct  /^ Function,   r_op: %fctType,
                                   r_args: %fctArgs,  r_result: %fctResult ) ];

//With the following definitions:
  Thing_that_can_be_represented_via_a_functional_relation
    has_descr_instrument<=: a Functional_relation, //actually "=:", not just "<=:" but "=: a ..."
    <=> (Thing_that_can_be_represented_via_a_function,         // cannot be translated to RIF-BLD
          has_descr_instrument<=: a Function );                // without skolem functions


/* In RIF-BLD/RIF-PS:

Forall ?t  ?fct ?fctType ?fctArgs ?fctResult  ?fRel ?fRelType ?fRelArg1 ?fRelArgsExcept1st (
  And ( ?fctArgs = ?fRelArg1      ?fctResult = ?fRelArgsExcept1st )
  :- And( ?t [rdf:type->Thing_that_can_be_represented_via_a_functional_relation
              rdf:type->Thing_that_can_be_represented_via_a_function
              r_descr_instrument->?fct     r_descr_instrument->?fRel ]
          ?fRel[r_op->?fRelType  r_args->List(?fRelArg1 | ?fRelArgsExcept1st)]
          ?fct[r_op->?fctType    r_args->?fctArgs  r_result->?fctResult] ) )
           
//With the following definitions:

  Forall ?t ?fRel (
  ?t[rdf:type->Thing_that_can_be_represented_via_a_functional_relation]
   :-  And ( ?t[has_descr_instrument->?fRel]  ?fRel[rdf:type->Functional_relation] ) )
  
  Forall ?t ?fct (
    ?t[rdf:type->Thing_that_can_be_represented_via_a_function]
     :-  And ( ?t[has_descr_instrument->?fct]  ?fct[rdf:type->Function] ) )

  Forall ?t (
    ?t[rdf:type->Thing_that_can_be_represented_via_a_functional_relation]
     :- ?t[rdf:type->Thing_that_can_be_represented_via_a_function] )
  Forall ?t (
    ?t[rdf:type->Thing_that_can_be_represented_via_a_function]
     :- ?t[rdf:type->Thing_that_can_be_represented_via_a_functional_relation] )