Specification of particular KRL abstract models

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

0.  Relations between particular KRL (abstract) models     (figure)

1.  Predicate Logic based particular models
    1.1.  First-order Logic (FOL) based particular models
        1.1.1.  Common Logics (CL)
    1.2.  Higher-Order Logic (HOL) based particular models
    1.3.  The RIF models

2.  Conjunctive existential formula based models
    2.1.  RDF, OWL and their variations (JSON-LD, OWL profiles, ...)




0.  Relations between particular KRL (abstract) models     (figure)


KRL_model = KRL_abstract_model,
/*/^ Language_abstract-model,  //already in ../o_KRLmodelTop/d_KRLmodelsTop.html */
  \. exclusion
     { (Propositional-logic_model
       )
       (Predicate-logic_model
         r_sub_KRL_model: Propositional-logic_model,
         \. exclusion
            { (Predicate-logic_model_less_expressive_than_1st-order-logic
                \. Description_logic_model_that_is_less_expressive_than_1st-order-logic
                   //to avoid discussions about modal operators and extended description logics
              )
              (First-order-logic_model = FOL_model,
                r_sub_KRL_model: Predicate-logic_model_less_expressive_than_1st-order-logic,
                \. partition
                   { (FOL_model_without_sets \. CL_model)
                     (FOL_model_with_sets \. KIF_model)
                   }
                   partition
                   { (FOL_model_without_meta-statements \. CL_model)
                     (FOL_model_with_meta-statements \. KIF_model)
                   }
                   partition
                   { (FOL_model_without_Henkin_interpretation \. CL_model)
                     (FOL_model_with_Henkin_interpretation \. KIF_model  FL_model,
                       r_sub_KRL_model: FOL_model_without_Henkin_interpretation )
                   } )
              (Higher-order-logic_model
                r_sub_KRL_model: FOL_model_with_Henkin_interpretation,
                \. RIF-FLD )
            } )
     }
     exclusion
     { (KRL-model_not_graph_based  //statement: 1 operator with its parameters
          \. (KRL-model_based_on_operators-with-parameters \. KIF_model)
       )
       (KRL-model_mostly_graph_based //statement: object + relations from/to it
          \. (KRL_model_mostly_based_on_a_graph_with_only_binary_relations
                \. (Frame_based_model
                     \. partition
                        { (Frame_model_with_closed_world_assumption \. F-Logic_classic_model)
                          (Frame_model_with_open_world_assumption \. Description_logic_model)
                        } )
                   (RDF_model = RDF)  (JSON-LD_model r_sub_KRL_model: RDF/*1.1*/)
                   (RDFS  r_sub_KRL_model: RDF)
                   ) )
             FL_model )
     } 
     (RIF \. RIF-Core  (RIF-BLD r_sub_KRL_model: RIF-Core) (RIF-FLD r_sub_KRL_model: RIF-BLD)
     )
     (Description_logic_based_model
       \. Description_logic_model_that_is_less_expressive_than_1st-order-logic
          (OWL_model = OWL,
            r_part_type: RDFS, //not semantic sub-model but structural sub-model (enough for '@')
            \. (OWL-1 = OWL1,
                 \. OWL1-Lite //follows the SHIF DL logic
                    (OWL1-DL   r_sub_KRL_model: OWL1-Lite)  //follows SHOIN(D)
                    (OWL1-Full r_sub_KRL_model: OWL1-DL  RDFS) )
               (OWL-2 = OWL2, r_sub_KRL_model: OWL-1,
                  \. OWL2-EL  OWL2-QL  OWL2-RL  //OWL2-EL follows EL++
                     (OWL2-DL //follows SROIQ(D), extends OWL1-DL and OWL2-EL
                        r_sub_KRL_model: OWL2-EL  OWL2-QL  OWL2-RL  OWL1-DL )
                     (OWL-2-Full  r_sub_KRL_model: OWL2_DL  OWL1-Full) )
          ) );




1.  Predicate Logic based particular models


1.1.  First-order Logic (FOL) based particular models


1.1.1.  Common Logics (CL)

See the ISO/IEC document of 2007 on CL.
 
Abstract_element@CL
  \. partition { NR_phrase@CL  Value_or_reference@CL }
     (AE_that_can_be_annotated_without_link@CL
        \.  cl#Text_construction  cl#Sentence  cl#Term  (cl#comment = Annotation@CL) )
     (Ordered_non-token_AE@CL /^ Positional_AE@CL); 

NR_phrase@CL
 \. partition  //CL is FOL, not HOL
    { (Modularizing_NR-phrase@CL
        \. partition
           { (Group_of_phrases@CL  //reminder: Document is head of a KRL grammar
               \. (Module@CL
                    = f_link_type _("",r_context,Module_body@CL,Module_context@CL),
                    \. (cl#text = Document@CL, 
                          \. partition{ cl#Text_construction
                                        cl#Domain_restriction  cl#Text_importation } )
                      %{ (cl#Named_module_that_may_have_submodules = cl#Module,
                            r_link_source: 0..* Module@CL,
                            r_link_destination: (a Module_context@CL 
                                                  r_part: a Module_name_link@CL) )
                         (cl#Module_that_may_not_have_submodules = cl#Text, 
                            r_link_source: 0 Module@CL)
                       } )
                  (Module_body@CL = cl#Text_construction cl#body_text) )
             (Modularizing_group-of-phrases_part@CL = cl#statement,
               \. partition
                  { (cl#Titling_statement = Module_name_link@CL)
                    (cl#Importation = Module_import_link@CL)
                    (cl#Discourse_statement /^ cl#Name_sequence,
                      \. partition
                         { (cl#Out_discourse_statement /^ Module_excluded_AE_link@CL)
                           cl#In_discourse_statement  
                         } )
                  } )
           } )
      (cl#Sentence = Formula@CL,
        \. partition
           { (Composite_formula@CL
               \. partition
                  { (cl#Boolean_sentence = Connective_formula@CL,
                      \. (Negating_formula@CL /^ Symmetric_negating_formula)
                    ) 
                    (cl#Quantified_sentence = First-order_logic_quantified_formula@CL)
                  } )
             (cl#Atom = NR_atomic_formula@CL,
                \. partition  
                   { (cl#Equation = Equal@CL
                                    f_link_type_("=",r_equal,cl#Term,cl#Term) )
                     (cl#Atomic_sentence = Relation@CL)
                   } )
             cl#Irregular_sentence
           } )
    };

Value_or_reference@CL 
 \. partition
    { (cl#Sequence_marker = Variable@CL,
         /^ Explicitly_bound_variable  Variable_not_referring_to_a_relation_type )
      (cl#Term = Value_or_referring_AE-that-is-not-a-variable@CL,
         \. partition
            { (cl#Functional_term = Non-aggregate_function_call@CL)  //e.g., a list?
              (cl#Name  //e.g., a datatype such as an integer!
                = Value_or_referring_AE_that_is_not_a_variable_nor_a_function_call@CL )
            } )  
    };



1.2.  Higher-Order Logic (HOL) based particular models

KRLO is based on a HOL model (even though the operator+arguments relations enable to describe the structures in RIF-BLD). The descriptions of HOL models will require less "restrictions" (w.r.t. the top-level of KRLO) than less expressive models.



1.3.  The RIF models

Sources: RIF-FLD RIF-PS grammar, RIF-BLD RIF-PS grammar, RIF-Core RIF-PS grammar.

Abstract_element@RIF-FLD
  \. (AE_that_can_be_annotated_without_link@RIF-FLD
       \. NR_phrase@RIF-FLD  rif-fld#Term )
     (Annotation_body@RIF-FLD
       \. (Annotation_body@RIF-BLD r_arg =: a AE@RIF-BLD
            \. Annotation_body@RIF-Core r_arg =: a AE@RIF-Core ),
       r_operator: 0..1 Constant@RIF-FLD,
       r_arg =: 0..1 Or{Minimal-frame_as_NR-phrase@RIF-FLD,
                          .{1..* Minimal-frame_as_NR-phrase@RIF-FLD} } )
     (rif-fld#Termula
       \. partition { NR_formula@RIF-FLD  rif-fld#Term } );


Modularizing_NR-phrase@RIF-FLD
 \. (Modularizing_NR-phrase@RIF-Core = Modularizing_NR-phrase@RIF-BLD,
      \. partition 
         { (Group_of_phrases@RIF-Core = Group_of_phrases@RIF-BLD,
             \. partition
                { (Document@RIF-Core = f_link_type_("",r_context,Module_body@RIF-Core,
                                                    Module_context@RIF-Core) )
                  (rif#Group = Module_that_may_have_submodules@RIF-Core,
                    /^ Module_body@RIF-Core,
                    r_link_source=: Or{rif#Group,rif-core#Rule} )
                  (Module_context@RIF-Core 
                    = f_relation_type _("",r_and,
                                       .[0..* Link_in_module_context@RIF-Core]) )
                } )
           Link_in_module_context@RIF-Core
         } )
    partition 
    { (Group_of_phrases@RIF-FLD
        \. partition
           { //The next line can be left implicit since it is automatically derived:
             //(Document@RIF-FLD = f_link_type_("",r_context,Module_body@RIF,Module_context@RIF-FLD))
             (rif-fld#Group = Module_that_may_have_submodules@RIF-FLD,
               /^ Module_body@RIF-FLD,
               r_link_source=: Or{rif#Group,rif#Formula} )
             (Module_context@RIF-FLD 
                = f_relation_type _("",r_and,.[0..* Link_in_module_context@RIF-FLD]) ) 
          } )
      (Link_in_module_context@RIF-FLD,
        \. partition
           { (Link_in_module_context@RIF-BLD = Link_in_module_context@RIF-Core,
               \. (rif#Base   = Module_base_IRI_link@RIF-Core)
                  (rif#Prefix = Module_context_namespace-definition_link@RIF-Core)
                  (rif#Import = Module_import_link@RIF-Core) )
             (rif#Dialect = Module_dialect_link@RIF-FLD)
             (rif#Module = Remote_module_naming_link@RIF-FLD)
           } )
    }
    (Annotation_link@RIF-FLD
      /^ f_link_type _("",r_annotation,Formula@RIF-FLD,Annotation_body@RIF-FLD) );



Formula@RIF-FLD //formulas can be term(ula)s, i.e., reified
 \. (Formula@RIF-BLD
      \. (Formula@RIF-Core 
           \. partition { NR_formula@RIF-Core  Reference_to_formula@RIF-Core } )
         partition { NR_formula@RIF-BLD  Reference_to_formula@RIF-BLD } )
    partition { NR_formula@RIF-FLD  Reference_to_formula@RIF-FLD };
    (rif-fld#Atomic 
      \. (rif-bld#Atomic = NR_atomic_formula@RIF-BLD,
           \. (rif-core#Atomic 
                \. partition { rif-core#Atom Minimal-frame_as_NR-phrase@RIF-Core } ) )
         partition { NR_atomic_formula@RIF-FLD  Reference_to_formula@RIF-FLD }
    ); 

NR_formula@RIF-FLD = f_relation_type _("",r_relation,.[1..* Formula@RIF-FLD]),
 \. partition
    { (Composite_formula@RIF-FLD
        \. (Composite_formula@RIF-BLD
             \. (Composite_formula@RIF-core
                  \. partition{rif-core#Rule rif-core#Composite_formula_but_not_rule} )
                partition {rif-bld#Rule rif-bld#Composite_formula_but_not_rule} )
           partition { Connective_formula@RIF-FLD  Classic_quantified_formula@RIF-FLD } )
      (NR_atomic_formula@RIF-FLD
        \. partition
           { (Non_frame_NR_atomic_formula@RIF-FLD
               /^ f_relation_type _("",r_relation,.[1..* rif-fld#Termula]),
               \. NR_atomic_formula@RIF-BLD
                  partition
                  { (Equal@RIF-FLD
                      /^ f_link_type_("=",r_equal,rif-fld#Termula,rif-fld#Termula),
                      \. (Equal@RIF-BLD r_arg =: a rif-bld#Term,
                           \. Equal@RIF-Core r_arg =: a rif-core#Term ) )
                    (Typing@RIF-FLD
                      = f_link_type_("#",r_type,rif-fld#Termula,rif-fld#Termula),
                      \. (Typing@RIF-BLD r_arg =: a rif-bld#Term,
                           \. Typing@RIF-Core r_arg =: a rif-core#Term ) )
                    (Supertyping@RIF-FLD
                      = f_link_type_("##",r_supertype,rif-fld#Termula,rif-fld#Termula),
                      \. (Supertyping@RIF-BLD r_arg =: a rif-bld#Term,
                           \. Supertyping@RIF-Core r_arg =: a rif-core#Term ) )
                    (rif-fld#Atom
                      /^ f_relation_type_("",r_relation,.[1..* rif-fld#Termula]),
                      \. (rif-bld#Atom 
                           r_arg =: a rif-bld#Term, 
                           \. (rif-core#Atom          
                                /^ f_relation_type_("",r_relation,.[1..* rif-core#Term]))
                              partition
                              { (rif-fld#Atom_with_named_arguments
                                  /^ Language_element_with_named_arguments )
                                (rif-fld#Atom_with_positional_arguments
                                  /^ Positional_language_element )
                              } ) ) 
                  } )               
             (Minimal-frame_as_NR-phrase@RIF-FLD
                \. Minimal-frame_as_NR-phrase@RIF-BLD,
                r_frame_head: 1 rif-fld#Termula,
                r_args: .[0..* ^(Minimal_half-link@RIF-FLD  r_op: 1 rif-fld#Termula,
                                      r_link_destination: 1 rif-fld#Termula) ] )
           } )
    }
    (NR_formula@RIF-BLD
      \. (NR_formula@RIF-Core
           \. partition { Composite_formula@RIF-Core  NR_atomic_formula@RIF-Core } )
         partition
         { (rif-bld#Rule  
             \. (rif-core#Rule 
                  \. partition { rif-core#Non-quantified_clause
                                 rif-core#Quantified_clause} )
                partition
                { (rif-bld#Non-quantified_clause
                    \. (rif-core#Non-quantified_clause)
                       partition
                       { (rif-bld#Atomic_clause /^ rif-bld#Atomic,
                           \. (rif-core#Atomic_clause /^ rif-core#Atomic) )
                         (rif-bld#Implies
                           \. (rif-core#Implies
                                \. partition { rif-core#Atomic_implies
                                               rif-bld#Non-atomic_implies } )
                              partition
                              { (rif-bld#Atomic_implies /^ rif-bld#Atomic,
                                  \. (rif-core#Atomic_implies /^ rif-core#Atomic) )
                                (rif-bld#Non-atomic_implies //And(ATOMIC*):-FORMULA
                                  = f_Link_type_(":-",r_rule-implication_of,
                                          rif-bld#And_of_atomic,rif-bld#Formula )
                                  \. (rif-core#Non-atomic_implies 
                                       = f_Link_type_(":-",r_rule-implication_of,
                                                      rif-core#And_of_atomic,
                                                      rif-core#Formula ) ) )
                              } ) 
                       } )  
                  (rif-bld#Quantified_clause
                    = f_quantification_type_("Forall",q_forall,.[],
                                         Variable_not_referring_to_a_phrase,
                                         rif-bld#Non-quantified_clause )
                    \. (rif-core#Quantified_clause
                         = f_quantification_type_("Forall",q_forall,.[],
                                         Variable_not_referring_to_a_phrase,
                                         rif-core#Non-quantified_clause ) ) )
                } )
           (rif_bld#Formula  //= rif_core#Formula + rif-bld#Subclass
             \. (rif_core#Formula
                  \. partition { rif-core#Composite_formula_but_not_rule
                                 NR_atomic_formula@RIF-Core } )
                partition
                { (rif-bld#Composite_formula_but_not_rule
                    \. (rif-core#Composite_formula_but_not_rule
                         \. partition
                            { (f_relation_type_("And",r_and,.[1..* rif_core#Formula])
                                \. (rif-core#And_of_atomic
                                    = f_relation_type_("And",r_and,
                                                       .[1..* rif_core#Atomic] ) ) )
                              f_relation_type_("Or",r_or,.[1..* rif_bld#Formula])
                              f_quantification_type_("Exists",q_exists,.[],
                                                     rif#Variable,rif_core#Formula )
                            } )
                       partition
                       { (f_relation_type_("And",r_and,.[1..* rif_bld#Formula])
                           \. (rif-bld#And_of_atomic
                                = f_relation_type_("And",r_and,.[1..* rif_bld#Atomic])))
                         f_relation_type_("Or",r_or,.[1..* rif_bld#Formula])
                         f_quantification_type_("Exists",q_exists,.[],rif#Variable,
                                                rif_bld#Formula )
                       } )
                  (NR_atomic_formula@RIF-BLD
                    \. (NR_atomic_formula@RIF-Core 
                         \. partition { Non_frame_NR_atomic_formula@RIF-Core
                                        Minimal-frame_as_NR-phrase@RIF-Core } )
                       partition
                       { (Non_frame_NR_atomic_formula@RIF-BLD
                           /^ f_relation_type _("",r_relation,.[1..* rif-bld#Term]),
                           \. (Non_frame_NR_atomic_formula@RIF-Core
                                /^ f_relation_type_("",r_relation,.[1..* rif-core#Term]),
                                \. partition
                                   { (Non_frame_NR_atomic_formula@RIF-Core
                                       \. partition{ Equal@RIF-Core  Typing@RIF-Core
                                                     rif-core#Atom } )
                                     Minimal-frame_as_NR-phrase@RIF-Core
                                   } )
                              partition
                              { (Non_frame_NR_atomic_formula@RIF-BLD
                                  \. Non_frame_NR_atomic_formula@RIF-Core
                                     partition { Equal@RIF-BLD  Typing@RIF-BLD
                                                 Supertyping@RIF-BLD  rif-bld#Atom } )
                                Minimal-frame_as_NR-phrase@RIF-BLD
                              } )
                         (Minimal-frame_as_NR-phrase@RIF-BLD 
                           \. (Minimal-frame_as_NR-phrase@RIF-Core
                                 r_frame_head: 1 rif-core#Term,
                                 r_args: .[0..* ^(Minimal_half-link@RIF-Core 
                                             r_op: 1 rif-core#Term,
                                             r_link_destination: 1 rif-core#Term ) ] ),
                            r_frame_head: 1 rif-bld#Term,
                            r_args: .[0..* ^(Minimal_half-link@RIF-BLD 
                                              r_op: 1 rif-bld#Term,
                                              r_link_destination: 1 rif-bld#Term ) ] )
                       } )
                 } )
         } )
    (Frame_or_Frames@RIF-FLD
      \. partition
         { Minimal-frame_as_NR-phrase@RIF-FLD 
           f_relation_type_("And",r_and,.[1..* Minimal-frame_as_NR-phrase@RIF-FLD])
         } );



rif-fld#Term = Value_or_reference@RIF-FLD,
 \. (rif-bld#Term 
      \. (rif-core#Term
           \. (rif-core#Grounded_term
                \. partition { rif-core#non-external_term
                               rif-core#Grounded_external_term } )
              partition { rif-core#non-external_term  rif-core#External_term } )
         partition { rif-bld#non-external_term  rif-bld#External_term }
    )
    partition
    { (rif-fld#non-external_term
        \. (rif-bld#non-external_term
             \. (rif-core#non-external_term
                  \. partition { rif-core#Const  rif-core#Var  rif-core#List } )
                partition { rif-core#Const rif-core#Var rif-bld#List rif-bld#Expr } )
           exclusion
           { (rif-core#Const = Constant@RIF-FLD Constant@RIF-BLD Constant@RIF-Core )
             (rif-fld#Var /^ Explicitly_bound_variable@RIF-FLD,
               \. rif-core#Var /^ Variable_not_referring_to_a_phrase@RIF-BLD )
             (rif-fld#List = List@RIF-FLD,  r_arg=: 1..* rif-fld#Term,
               \. (rif-bld#List = List@RIF-FLD,  r_arg=: 1..* rif-bld#Term,
                    \. (rif-core#List = Closed_list@RIF-Core,
                          r_arg=: 1..* rif-core#Grounded_term ) )
                  partition { Closed_list@RIF-FLD Open_list@RIF-FLD } )
             (Function_call@RIF-FLD /^ Function_call_with_possible_name_parameters@RIF-FLD,
               \. partition
                  { (rif-fld#Expr /^ Non-aggregate_function_call@RIF-FLD,
                      r_arg =: 1..* rif-bld#Term,
                      \. (rif-bld#Expr /^ Positional_function_call@RIF-Core,
                           /^ f_function-call_type("",rif-core#Const,.[1..* rif-core#Term],
                                                   "" ) ) )
                    (rif-fld#Aggregate = Aggregate_function_call@RIF-FLD,
                      r_args: .[1..* rif-fld#Var, NR_formula@RIF-FLD] )
                  }
                  partition
                  { (Positional_function_call@RIF-FLD
                       = f_function-call_type("",rif-fld#Termula,.[1..* rif-fld#Termula],
                                             ) )
                    (Function_call_with_named_parameter@RIF-FLD
                       = f_function-call_type(rif-core#Name,rif-fld#Termula,
                                              .[1..* rif-fld#Termula] ) )
                  } )
           } )
      (rif-fld#External_term = Structured_reference_to_externally_defined_AE@RIF-FLD,
        \. partition
           { (rif-fld#External_formula
                /^ f_frame_as_ref_("External",r_external_reference,
                                   .[1 rif-fld#Atomic, 1 rif-fld#Locator] ) )
             (rif-fld#External_non-formula_term
                /^ f_frame_as_ref_("External",r_external_reference,
                                   .[1 rif-fld#Expric, 1 rif-fld#Locator] ),
                \. (rif-bld#External_term
                     /^ f_frame_as_ref_("External",r_external_reference,rif-bld#Expr),
                     \. (rif-core#External_term
                          /^ f_frame_as_ref_("",r_external_reference,rif-core#Expr),
                          \. (rif-core#Grounded_external_term 
                               /^ f_frame_as_ref_("External",r_external_reference,
                                                  rif-core#Grounded_expr ) ) )
                   ) )
           } )
    };


Reference_to_formula@RIF-FLD r_result=: 1 Formula@RIF-FLD,
 \. (Reference_to_formula@RIF-BLD r_result=: 1 Formula@RIF-BLD,
     \. (Reference_to_formula@RIF-Core  r_result=: 1 Formula@RIF-Core) )
    partition
    { Formula_referring_token@RIF-FLD  
      (Structured_reference_to_formula@RIF-FLD
        \. partition 
           { Function_call_returning_a_formula@RIF-FLD
             Frame_as_reference_to_formula@RIF-FLD
             Structured_reference_to_formula_from_a_remote_module@RIF-FLD  //same KRL
             Structured_reference_to_externally_defined_formula@RIF-FLD //another KRL
           } )
    };




2.  Conjunctive existential formula based models

Abstract_element@Conjunctive-existential-formula_based_model
  \. partition
     { (Formula@Conjunctive-existential-formula_based_model
         \. partition
            { (Composite_formula@Conjunctive-existential-formula_based_model
                \. partition
                   { Conjunction_of_formulas@Conjunctive-existential-formula_based_model
                     Existentially_quantified_formula@Conjunctive-existential-formula_based_model
                   } )
              NR_atomic_formula@Conjunctive-existential-formula_based_model
            } )
       Value_or_reference@Conjunctive-existential-formula_based_model
     };


2.1.  RDF, OWL and their variations (JSON-LD, OWL profiles, ...)

rdfs#Resource = owl#Thing  Thing, 
 \. (Abstract_element@RDF
       /^ Abstract_element@Conjunctive-existential-formula_based_model,
       \. partition
          { (NR_phrase@RDF
              \. partition
                 { Modularizing_NR-phrase@RDF
                   (NR_formula@RDF = rdf#Statement, 
                     \. partition
                        { (NR-Composite_formula@RDF
                            \. partition { Conjunction_of_formulas@RDF
                                           Existentially_quantified_formula@RDF } )
                          NR_link@RDF
                        } )
                 } )
            Value_or_reference@RDF   
          } 
          (Abstract_element@OWL
            \. partition
               { (NR_phrase@OWL
                   \. partition
                      { (Modularizing_NR-phrase@OWL
                          \. partition
                             { (Group_of_phrases@OWL
                                 \. //The next 2 lines are implicit since automatically derived:
                                    //(Document@OWL = f_link_type_("",r_context,Module_body@OWL,
                                    //                                          Module_context@OWL))
                                    (owl#Ontology = Module_body@OWL)  owl#Ontology_Importation )
                               (Link_in_module_context@OWL
                                 \. Module_IRI_link@OWL  Module_version_link@OWL 
                                    Module_import_link_with_IRI@OWL  Module_annotation_link )
                             } )
                        (owl#Axiom /^ NR_atomic_formula@OWL) //see below
                      } )
                 Value_or_reference@OWL  //see below
               }
               (owl#Thing_refered_by_an_IRI = owl#Entity,  r_reference=: 1 IRI,
                 \. owl#NamedIndividual  rdfs#Class  rdfs#Datatype
                    owl#ObjectProperty  owl#DataProperty  owl#AnnotationProperty )
               partition 
               { (Individual@RDF
                   \. partition
                      { (owl#NamedIndividual = Individual@OWL2-EL  Individual@OWL2-QL,
                           = ^(Individual@RDF r_reference: 1 IRI))
                        (owl#AnonymousIndividual = ^(Individual@RDF
                                                       r_reference: 1 Sparql_blank-node_ID ))
                      } )
                 r_relation@RDF  //see below
                 (Type@RDF \. partition { Class@RDFS  Property_type@RDF })  //see below
               }
               partition 
               { AE_that_cannot_be_annotated_without_link@OWL
                 (AE_that_can_be_annotated_without_link@OWL
                   \. partition { ^(Thing  r_reference: 1 IRI)  owl#AnonymousIndividual } )
               }
               partition
               { AE_that_cannot_be_annotation_value@OWL
                 (AE_that_can_be_annotation_value@OWL
                   \. owl#AnonymousIndividual  IRI  rdfs#Literal )
               }
               partition
               { (Constant@RDF
                   \. (owl#IRI_for_type_of_basic_type-or-named-individual
                        = ^(IRI r_reference of:
                              ^(Type  r_instance: a owl#Thing_refered_by_an_IRI) ) )
                 Thing_that_is_not_a_constant@RDF
               }
          )
    );




owl#Axiom
 \. partition  
    { (owl#Declaration 
        = ^[a IRI  r_type: a owl#IRI_for_type_of_basic_type-or-named-individual] )
      (owl#ClassAxiom
         \. partition
            { (owl#SubClassOf = ^[a owl#SubClassExpression
                                   rdfs#subClassOf: a owl#SuperClassExpression ])
              (owl#EquivalentClasses
                = ^[an owl#AllEquivalentClasses  r_member: 2..* owl#SuperClassExpression],
                \. (owl#EquivalentClasses@OWL2-RL
                     = ^[an owl#AllEquivalentClasses  r_member: 2..* owl#EquivClassExpression] ) )
              (owl#DisjointClasses  
                = ^[an owl#AllDisjointClasses  r_member: 2..* owl#SuperClassExpression] )
              (owl#DisjointUnion 
                = ^[a owl#ObjectClass_IRI  owl#unionOf: an owl#AllDisjointClasses] ) 
            }
            (owl#ClassAxiom@OWL2-EL  //no owl#DisjointUnion 
              \. partition { owl#SubClassOf@OWL2-EL  owl#EquivalentClasses@OWL2-EL
                             owl#DisjointClasses@OWL2-EL } )
            (owl#ClassAxiom@OWL2-QL  //no owl#DisjointUnion 
              \. partition { owl#SubClassOf@OWL2-QL  owl#EquivalentClasses@OWL2-QL
                             owl#DisjointClasses@OWL2-QL  } )
            (owl#ClassAxiom@OWL2-RL  //no owl#DisjointUnion 
              \. partition { owl#SubClassOf@OWL2-RL  owl#EquivalentClasses@OWL2-RL
                             owl#DisjointClasses@OWL2-RL  } )
      )
      (owl#ObjectPropertyAxiom
        \. partition
           { (owl#SubObjectPropertyOf = ^[a owl#ObjectPropertyExpressionOrChain
                                           rdfs#subPropertyOf: a owl#ObjectPropertyExpression ],
               \. (owl#SubObjectSinglePropertyOf = ^[a owl#ObjectPropertyExpression
                                           rdfs#subPropertyOf: a owl#ObjectPropertyExpression ] ) )
             (owl#EquivalentObjectProperties  //owl#AllEquivalentProperties yet implicit in OWL 
               = ^[an owl#AllEquivalentProperties  r_member: 2..* owl#ObjectPropertyExpression] )
             (owl#DisjointObjectProperties  //owl#AllDisjointProperties implicit in OWL 
               = ^[an owl#AllDisjointProperties  r_member: 2..* owl#ObjectPropertyExpression]
             )                      //all members are owl#propertyDisjointWith of one another
             (owl#InverseObjectProperties = ^[a owl#ObjectPropertyExpression
                                               owl#inverseOf: a owl#ObjectPropertyExpression ])
             (owl#ObjectPropertyDomain = ^[a owl#ObjectPropertyExpression
                                            rdfs#domain: a owl#ClassExpression ],
               \. (owl#ObjectPropertyDomainSup = ^[a owl#ObjectPropertyExpression
                                                    rdfs#domain: a owl#SuperClassExpression ] ) )
             (owl#ObjectPropertyRange = ^[a owl#ObjectPropertyExpression
                                           rdfs#range: a owl#ClassExpression ],
               \. (owl#ObjectPropertyRangeSup = ^[a owl#ObjectPropertyExpression
                                                   rdfs#range: a owl#SuperClassExpression ] )
             )
             (owl#FunctionalObjectProperty = ^[a owl#ObjectPropertyExpression
                                                rdf#type: owl#FunctionalProperty ])
             (owl#InverseFunctionalObjectProperty = ^[a owl#ObjectPropertyExpression
                                                       rdf#type: owl#InverseFunctionalProperty ])
             (owl#ReflexiveObjectProperty = ^[a owl#ObjectPropertyExpression
                                               rdf#type: owl#ReflexiveProperty ])
             (owl#IrreflexiveObjectProperty = ^[a owl#ObjectPropertyExpression
                                                 rdf#type: owl#IrreflexiveProperty ])
             (owl#SymmetricObjectProperty = ^[a owl#ObjectPropertyExpression
                                               rdf#type: owl#SymmetricProperty ]) 
             (owl#AsymmetricObjectProperty = ^[a owl#ObjectPropertyExpression
                                                rdf#type: owl#AsymmetricProperty ]) 
             (owl#TransitiveObjectProperty = ^[a owl#ObjectPropertyExpression
                                                rdf#type: owl#AsymmetricProperty ])
           }
           (owl#ObjectPropertyAxiom@OWL2-EL 
             \. partition
                { owl#EquivalentObjectProperties@OWL2-EL  owl#SubObjectPropertyOf@OWL2-EL
                  owl#ObjectPropertyDomain@OWL2-EL        owl#ObjectPropertyRange@OWL2-EL
                  owl#ReflexiveObjectProperty@OWL2-EL     owl#TransitiveObjectProperty@OWL2-EL
                } ) /* no: owl#IrreflexiveObjectProperty  
                           owl#DisjointObjectProperties   owl#InverseObjectProperties
                           owl#FunctionalObjectProperty   owl#InverseFunctionalObjectProperty
                           owl#SymmetricObjectProperty    owl#AsymmetricObjectProperty */
           (owl#ObjectPropertyAxiom@OWL2-QL 
             \. partition
                { owl#EquivalentObjectProperties@OWL2-QL  owl#SubObjectSinglePropertyOf@OWL2-QL
                  owl#ObjectPropertyDomainSup@OWL2-QL //domain: owl#SuperClassExpression
                  owl#ObjectPropertyRangeSup@OWL2-QL  //range: owl#SuperClassExpression
                  owl#IrreflexiveObjectProperty@OWL2-QL //forgotten in official grammar!
                  owl#ReflexiveObjectProperty@OWL2-QL  //no: owl#TransitiveObjectProperty@OWL2-QL
                  /*yes*/owl#DisjointObjectProperties   owl#InverseObjectProperties
                         owl#SymmetricObjectProperty    owl#AsymmetricObjectProperty
                } ) //still no: owl#FunctionalObjectProperty   owl#InverseFunctionalObjectProperty
           (owl#ObjectPropertyAxiom@OWL2-RL 
             \. partition
                { owl#EquivalentObjectProperties@OWL2-RL  owl#SubObjectSinglePropertyOf@OWL2-RL
                  owl#ObjectPropertyDomainSup@OWL2-RL //domain: owl#SuperClassExpression
                  owl#ObjectPropertyRangeSup@OWL2-RL  //range: owl#SuperClassExpression
                  owl#IrreflexiveObjectProperty@OWL2-RL  /*no*/owl#ReflexiveObjectProperty@OWL2-RL
                  /*yes*/owl#TransitiveObjectProperty@OWL2-RL
                  /*yes*/owl#DisjointObjectProperties   owl#InverseObjectProperties
                         owl#SymmetricObjectProperty    owl#AsymmetricObjectProperty
                  /*+*/owl#FunctionalObjectProperty  owl#InverseFunctionalObjectProperty
                } ) 
      )
      (owl#DataPropertyAxiom
        \. partition
           { (owl#SubDataPropertyOf = ^[a owl#DataPropertyExpression
                                         rdfs#subPropertyOf: a owl#DataPropertyExpression ])
             (owl#EquivalentDataProperties  //owl#AllEquivalentProperties implicit in OWL 
               = ^[an owl#AllEquivalentProperties  r_member: 2..* owl#DataPropertyExpression] )
             (owl#DisjointDataProperties   //owl#AllDisjointProperties is implicit in OWL 
               = ^[an owl#AllDisjointProperties  r_member: 2..* owl#DataPropertyExpression]
             ) //owl#propertyDisjointWith
             (owl#DataPropertyDomain = ^[a owl#DataPropertyExpression
                                          rdfs#domain: a owl#ClassExpression ],
               \. (owl#DataPropertyDomainSup = ^[a owl#DataPropertyExpression
                                                  rdfs#domain: a owl#SuperClassExpression ] ) )
             (owl#DataPropertyRange  = ^[a owl#DataPropertyExpression
                                          rdfs#range: a owl#ClassExpression ],
               \. (owl#DataPropertyRangeSup = ^[a owl#DataPropertyExpression
                                                 rdfs#range: a owl#SuperClassExpression ] ) )
             (owl#FunctionalDataProperty = ^[a owl#DataPropertyExpression
                                              rdf#type: owl#FunctionalProperty ])
           }
           (owl#DataPropertyAxiom@OWL2-EL  //no owl#DisjointDataProperties
             \. owl#SubDataPropertyOf@OWL2-EL   owl#EquivalentDataProperties@OWL2-EL 
                owl#DataPropertyDomain@OWL2-EL owl#DataPropertyRange@OWL2-EL
                owl#FunctionalDataProperty@OWL2-EL )
           (owl#DataPropertyAxiom@OWL2-QL  //no owl#DisjointDataProperties
             \. owl#SubDataPropertyOf@OWL2-QL   owl#EquivalentDataProperties@OWL2-QL 
                owl#DataPropertyDomainSup@OWL2-QL owl#DataPropertyRangeSup@OWL2-QL
                /*owl#FunctionalDataProperty@OWL2-QL*/ owl#DisjointDataProperties@OWL2-QL )
           (owl#DataPropertyAxiom@OWL2-RL 
             \. owl#SubDataPropertyOf@OWL2-RL   owl#EquivalentDataProperties@OWL2-RL 
                owl#DataPropertyDomainSup@OWL2-RL 
                owl#DataPropertyRangeSup@OWL2-RL //Sup forgotten in official grammar?
                owl#FunctionalDataProperty@OWL2-RL //forgotten in official summary (grammar ok)?
                owl#DisjointDataProperties@OWL2-RL )
      )
      (owl#DatatypeDefinition = ^[a rdfs#Datatype  owl#equivalentClass: owl#DataRange])
      (owl#HasKey = ^[a owl#ClassExpression 
                       owl#hasKey: 0..* owl#ObjectPropertyExpression 
                                   0..* owl#DataPropertyExpression ],
        \. (owl#SubHasKey = ^[a owl#SubClassExpression 
                               owl#hasKey: 0..* owl#ObjectPropertyExpression 
                                           0..* owl#DataPropertyExpression ] ) )
      (owl#Assertion
        \. partition
           { (owl#ObjectPropertyAssertion
               = ^[an Individual@RDF, (a owl#ObjectPropertyExpression): an Individual@RDF] )
             (owl#NegativeObjectPropertyAssertion
               = ^[an Individual@RDF, not (a owl#ObjectPropertyExpression): an Individual@RDF],
               \. (owl#NegativeObjectPropertyAssertion@OWL2-DL //hence in OWL2-EL/QL/RL but the
                     = ^[a owl#NamedIndividual,       // OWL2-RL official grammar missed that!?
                           not (a owl#ObjectPropertyExpression): a owl#NamedIndividual ] ) )
             (owl#SameIndividual = ^[a  Same_things@OWL r_member: 2..* Individual@RDF],
               \. (owl#SameIndividual@OWL2-DL
                    = ^[a Same_things@OWL2-DL  r_member: 2..* owl#NamedIndividual] ) )
             (owl#DifferentIndividuals = ^[a Different_things@OWL r_member: 2..* Individual@RDF],
               \. (owl#DifferentIndividuals@OWL2-DL
                    = ^[a Different_things@OWL2-DL  r_member: 2..* owl#NamedIndividual] ) ))
             (owl#ClassAssertion = ^[a owl#ClassExpression r_instance: an Individual@RDF],
                \. owl#Super_ClassAssertion = ^[a owl#SuperClassExpression
                                                 r_instance: an Individual@RDF] 
             (owl#DataPropertyAssertion
               = ^[an Individual@RDF, (a owl#DataPropertyExpression): a rdfs#Literal] )
             (owl#NegativeDataPropertyAssertion
               = ^[an Individual@RDF, not (a owl#DataPropertyExpression): a rdfs#Literal],
               \. (owl#NegativeDataPropertyAssertion@OWL2-DL
                     = ^[a owl#NamedIndividual,
                           not(a owl#DataPropertyExpression): a rdfs#Literal ] ) )
           }
           (owl#Assertion@OWL2-QL   //no: owl#Negative(Object/Data)PropertyAssertion
             \. partition           //no: owl#SameIndividual
                { owl#ObjectPropertyAssertion@OWL2-QL  owl#DifferentIndividuals@OWL2-QL
                  owl#ClassAssertion@OWL2-QL  owl#DataPropertyAssertion@OWL2-QL
                } )
           (owl#Assertion@OWL2-RL   //no: owl#Negative(Object/Data)PropertyAssertion
             \. partition           //no: owl#SameIndividual
                { owl#ObjectPropertyAssertion@OWL2-RL  owl#DifferentIndividuals@OWL2-RL
                  owl#Super_ClassAssertion@OWL2-RL  owl#DataPropertyAssertion@OWL2-RL
                  /*+*/ owl#SameIndividual@OWL2-RL  owl#NegativeObjectPropertyAssertion@OWL2-RL
                        owl#NegativeDataPropertyAssertion@OWL2-RL
                } ) )
      (owl#AnnotationAxiom
        \. partition
           { (owl#AnnotationAssertion
                = ^[an AE_that_can_be_annotated_without_link@OWL
                    (a owl#AnnotationProperty): an AE_that_can_be_annotation_value@OWL ] )
             (owl#SubAnnotationPropertyOf
                = ^[a owl#AnnotationProperty  rdfs#subPropertyOf: a owl#AnnotationProperty] )
             (owl#AnnotationPropertyDomain 
                = ^[a owl#AnnotationProperty  rdfs#domain: a owl#ObjectClass_IRI] )
             (owl#AnnotationPropertyRange
                = ^[a owl#AnnotationProperty  rdfs#range:  a owl#ObjectClass_IRI] )
           } )
    } /*
    (owl#Axiom@OWL2-EL  //useless since no selection of direct subtypes:
      \. partition
         { owl#ClassAxiom@OWL2-EL  owl#ObjectPropertyAxiom@OWL2-EL  owl#DataPropertyAxiom@OWL2-EL
           owl#Assertion@OWL2-EL owl#HasKey@OWL2-EL//these 2 and next 3: not restricted in OWL2-EL
           owl#DatatypeDefinition@OWL2-EL  owl#Declaration@OWL2-EL  owl#AnnotationAxiom@OWL2-EL
         } ) */
    (owl#Axiom@OWL2-QL  //no: owl#HasKey 
      \. partition
         { owl#ClassAxiom@OWL2-QL  owl#ObjectPropertyAxiom@OWL2-QL  owl#DataPropertyAxiom@OWL2-QL
           owl#Assertion@OWL2-QL  //the next 3 are not restricted in OWL2-QL:
           owl#DatatypeDefinition@OWL2-QL  owl#Declaration@OWL2-QL  owl#AnnotationAxiom@OWL2-QL
         } )
    (owl#Axiom@OWL2-RL
      \. partition
         { owl#ClassAxiom@OWL2-RL  owl#ObjectPropertyAxiom@OWL2-RL  owl#DataPropertyAxiom@OWL2-RL
           owl#Assertion@OWL2-RL  owl#SubHasKey@OWL2-RL  //next 3 not restricted in OWL2-RL:
           owl#DatatypeDefinition@OWL2-RL  owl#Declaration@OWL2-RL  owl#AnnotationAxiom@OWL2-RL
         } );


Value_or_reference@RDF
 \. partition
    { (rdfs#Literal = Value_token@RDF, //note: any rdfs#Datatype is subclass of rdfs#Literal
        \. (rdf#langString = Language-tagged_string_value)
           rdf#HTML  rdf#XMLLiteral )
      (Reference_or_structured-value_or_type@RDF
        \. partition
           { (Referring_token@JSON-LD_model
                /^ Implicitly_existentially_bound_variable  Absolute_identifier,
                \. partition { IRI@JSON-LD_model  Blank_node_identifier@JSON-LD_model } )
             Frame_as_reference@JSON-LD_model
           }
           partition
           { Type@RDF
             (Referring_individual_AE@RDF
               \. partition
                  { Referring_token@RDF
                    (Structured_referring_AE@RDF
                      \. (Collection@RDF
                           \. (rdf#List \.. (rdf#nil = Null_list@RDF))
                              (rdfs#Container = Collection@RDF,
                                \. partition { (rdf#Bag = Bag@RDF)  (rdf#Seq = Sequence@RDF)
                                               (rdf#Alt = List_of_alternatives) } )
                              (Collection_of_types@OWL
                                \. (Disjoint_types@OWL
                                     \. (owl#AllDisjointClasses
                                           r_member=: 2..* owl#ClassExpression)
                                        (owl#AllDisjointProperties  //yet implicit in OWL 
                                           r_member=: 2..* Property_type@RDF ) )
                                   (Equivalent_types@OWL  //although yet implicit in OWL 
                                     \. (owl#AllEquivalentClasses
                                           r_member=: 2..* owl#ClassExpression)
                                        (owl#AllEquivalentProperties
                                           r_member=: 2..* Property_type@RDF) )
                                   Same_things@OWL  Different_things@OWL )
                         )
                         (Component_of_an_AE_that_is_not_an_NR-phrase@OWL
                           \. (owl#Datarange_restriction
                                 r_part: owl#ConstrainingFacet owl#RestrictionValue )
                              owl#ConstrainingFacet 
                              owl#RestrictionValue )
                    )
                  } )
           } )
    };  

  
Class@RDFS  = Concept_type@RDFS,  != rdfs#Class, 
 \. partition
    { (rdfs#IRI_for_Concept_type = ^(IRI r_reference of: Class@RDFS),
        \. partition
           { (owl#ObjectClass_IRI = ^(IRI  r_reference of: a owl#ClassExpression),
                   //hence (next line), en OWL FSS:
                = ^(IRI  r_declaration_with_type@OWL =: the rdfs#IRI_for_Concept_type), 
                \. (owl#Thing_IRI = ^(IRI r_reference of: a owl#Thing)) )
             (owl#Datatype_IRI = ^(IRI  r_reference of: a rdfs#Datatype))
           } )
      owl#Class_or_datatype_expression_that_is_not_an_IRI
    }
    partition
    { (owl#ClassExpression
        \. (rdfs#Class = owl-full#Class,
             \. owl-dl#Class  (owl#Class_different_from_Thing != owl#Thing),
             \.. owl#Thing  owl#Nothing )
           owl#SubClassExpression  owl#SuperClassExpression
           (owl#EquivClassExpression
             \. partition
                { owl#ObjectClass_IRI_other_than_Thing   owl#ObjectHasValue  owl#DataHasValue
                  owl#EquivObjectIntersectionOf 
                } )
           partition
           { (owl#ObjectClass_IRI = owl#Class,
               \. (owl#ObjectClass_IRI_other_than_Thing != owl#Thing_IRI) )
             (owl#Restriction /^ Anonymous_type,  
               \. partition
                  { (owl#ClassExpression_to_classCollection 
                       \. partition
                          { (owl#ObjectIntersectionOf 
                               = ^(owl#ClassExpression
                                     owl#intersectionOf=: .{2..* owl#ClassExpression} ),
                               \. (owl#SubObjectIntersectionOf = ^(owl#SubClassExpression
                                          owl#intersectionOf=: .{2..* owl#SubClassExpression} ) )
                                  (owl#SuperObjectIntersectionOf = ^(owl#SuperClassExpression
                                          owl#intersectionOf=: .{2..* owl#SuperClassExpression} ) )
                                  (owl#EquivObjectIntersectionOf = ^(owl#SuperClassExpression
                                          owl#intersectionOf=: .{2..* owl#EquivClassExpression} ) )
                            )
                            (owl#ObjectUnionOf 
                               = ^(owl#ClassExpression  owl#unionOf=: .{2..* owl#ClassExpression}),
                               \. (owl#SubObjectUnionOf = ^(owl#SubClassExpression
                                          owl#unionOf=: .{2..* owl#SubClassExpression} ) )
                                  (owl#SuperObjectUnionOf = ^(owl#SuperClassExpression
                                          owl#unionOf=: .{2..* owl#SuperClassExpression} ) ) )
                          } )
                    (owl#ObjectComplementOf
                      = ^(owl#ClassExpression  owl#complementOf=: 1 owl#ClassExpression),
                      \. (owl#SuperObjectComplementOf  //uses SubClassExpression as noted in
                                 // https://www.w3.org/TR/owl2-profiles/#Class_Expressions_3
                           = ^(owl#ClassExpression  owl#complementOf=: 1 owl#SubClassExpression)
                         ) )
                    (owl#ObjectOneOf
                      = ^(owl#ClassExpression  owl#oneOf=: .{1..* owl#Individual@RDF}),
                      \. (owl#ObjectOneOf1Individual= ^(owl#ClassExpression 
                                                          owl#oneOf=: .{1 owl#Individual@RDF} ) )
                         (owl#ObjectOneOf@OWL2-DL  owl#oneOf=: .{1..* a owl#NamedIndividual}) )
                    (owl#PropertyRestriction 
                      = ^(owl#ClassExpression //owl#Thing if implicit, e.g., in ObjectMaxCardin.
                            owl#onProperty =: 1 Property_type@RDF,
                            owl#onProperty_restriction=: 1 owl#Thing ),
                      \. partition
                         { (owl#ObjectPropertyRestriction
                             = ^(owl#PropertyRestriction
                                   owl#onProperty =: 1 owl#ObjectPropertyExpression ),
                             \. partition
                                { (owl#ObjectAllValuesFrom 
                                     owl#allValuesFrom=: 1 owl#ClassExpression,
                                     \. (owl#SuperObjectAllValuesFrom
                                           owl#allValuesFrom=: 1 owl#SuperClassExpression ) )
                                  (owl#ObjectSomeValuesFrom 
                                     owl#someValuesFrom=: 1 owl#ClassExpression,
                                     \. (owl#ObjectSomeValuesFromThing
                                          owl#someValuesFrom=: 1 owl#Thing_IRI )
                                     \. (owl#SubObjectSomeValuesFrom
                                          owl#someValuesFrom=: 1 owl#SubClassExpression ) )
                                  (owl#ObjectHasValue  owl#hasValue=: 1 owl#Individual,
                                     \. (owl#ObjectHasValue@OWL2-DL
                                           owl#hasValue=: 1 owl#NamedIndividual ) )
                                  (owl#ObjectHasSelf   owl#hasSelf=:  1 xsd#boolean)
                                }
                           )
                           (owl#ObjectPropertyCardinalityRestriction  = ^(owl#PropertyRestriction
                                  owl#r_relation_from_restriction_to_nonNegativeInteger =:
                                                                        1 xsd#nonNegativeInteger ),
                             \. partition
                                { owl#(ObjectMinCardinality
                                     owl#minCardinality=: 1 xsd#nonNegativeInteger )
                                  (owl#ObjectExactCardinality
                                     owl#cardinality=: 1 xsd#nonNegativeInteger )
                                  (owl#ObjectMaxCardinality
                                     owl#maxCardinality=: 1 xsd#nonNegativeInteger,
                                     \. (owl#SuperObjectMaxCardinality
                                           owl#maxCardinality=: 0..1 xsd#nonNegativeInteger,
                                           \. partition
                                              { (owl#SuperObjectMaxCardinalityWithExpressionAsSource
                                                   /^ owl#SubClassExpression )  //strange but ok
                                                (owl#SuperObjectMaxCardinalityWithThingAsSource
                                                   /^ owl#Thing_IRI )  //strange but ok
                                              } ) )
                                }
                           )
                           (owl#DataPropertyRestriction
                             = ^(owl#PropertyRestriction 
                                   owl#onProperty=: 1 owl#DataPropertyExpression),
                             \. partition
                                { (owl#DataAllValuesFrom   owl#allValuesFrom=: 1 owl#DataRange)
                                  (owl#DataSomeValuesFrom owl#someValuesFrom=: 1 owl#DataRange)
                                  (owl#DataHasValue  owl#hasValue=: 1 rdfs#Literal)
                                }
                           ) 
                           (owl#DataPropertyCardinalityRestriction = ^(owl#DataPropertyExpression
                                       owl#r_relation_from_restriction_to_nonNegativeInteger =:
                                                                       1 xsd#nonNegativeInteger ),
                             \. partition
                                { (DataMinCardinality owl#minCardinality=: 1 xsd#nonNegativeInteger)
                                  (DataExactCardinality  owl#cardinality=: 1 xsd#nonNegativeInteger)
                                  (DataMaxCardinality owl#maxCardinality=: 1 xsd#nonNegativeInteger,
                                    \. (SuperDataMaxCardinality
                                          owl#maxCardinality=: 0..1 xsd#nonNegativeInteger ) )
                                } )
                         }
                         (owl#PropertyCardinalityRestriction
                           \. partition { owl#ObjectPropertyCardinalityRestriction
                                          owl#DataPropertyCardinalityRestriction } )
                    )//end of owl#PropertyRestriction
                  }                  
                  (owl#Restriction@OWL2-EL  
                    \. partition
                       { //no:  disjunction (ObjectUnionOf, DisjointUnion, and DataUnionOf)
                         //     enumerations of more than 1 indiv. (ObjectOneOf and DataOneOf) 
                         //     class negation (ObjectComplementOf), cardin.(just All...) 
                         owl#ObjectIntersectionOf@OWL2-EL
                         owl#ObjectOneOf1Individual@OWL2-EL 
                         //owl#PropertyRestriction@OWL2-EL:  //no cardin, owl#ObjectAllValuesFrom
                              owl#ObjectSomeValuesFrom@OWL2-EL
                              owl#ObjectHasValue@OWL2-EL  owl#ObjectHasSelf@OWL2-EL
                         //owl#DataPropertyRestriction@OWL2-EL  //no cardin, owl#DataAllValuesFrom
                              owl#DataSomeValuesFrom@OWL2-EL  owl#DataHasValue@OWL2-EL 
                       } )
                  (owl#Restriction@OWL2-QL
                    \. /* partition  //useless since Sub/Super-ClassRestriction
                       { //no:  disjunction (ObjectUnionOf, DisjointUnion, and DataUnionOf)
                         //     enumerations (ObjectOneOf and DataOneOf), cardin.(just Some...)
                         owl#ObjectIntersectionOf@OWL2-QL //this and the next 2 in SuperClassExpr
                         /*+*/owl#ObjectComplementOf@OWL2-QL
                         //owl#PropertyRestriction@OWL2-QL:
                             owl#ObjectSomeValuesFrom@OWL2-QL //from Thing when in SubClassExpr
                             owl#DataSomeValuesFrom@OWL2-QL //also in SuperClassExpr, despite what
                       }       // the official summary says (the official grammar is ok there)  */
                       partition
                       { (owl#SubClassRestriction@OWL2-QL
                           \. partition { owl#ObjectSomeValuesFromThing@OWL2-QL
                                          owl#DataSomeValuesFrom@OWL2-QL } )
                         (owl#SuperClassRestriction@OWL2-QL
                           \. partition
                              { owl#ObjectIntersectionOf@OWL2-QL  owl#ObjectComplementOf@OWL2-QL
                                owl#ObjectSomeValuesFrom@OWL2-QL  owl#DataSomeValuesFrom@OWL2-QL
                              } )
                       } )
                  (owl#Restriction@OWL2-RL
                    \. partition
                       { (owl#SubClassRestriction@OWL2-RL //+ disjunction, some, exact
                           \. partition
                              { owl#SubObjectIntersectionOf@OWL2-RL
                                owl#SubObjectUnionOf@OWL2-RL         owl#ObjectOneOf@OWL2-RL
                                owl#SubObjectSomeValuesFrom@OWL2-RL  owl#ObjectHasValue@OWL2-RL
                                owl#DataSomeValuesFrom@OWL2-RL       owl#DataHasValue@OWL2-RL
                              } )
                         (owl#SuperClassRestriction@OWL2-RL //+ negation, all, exact
                           \. partition
                              { owl#SuperObjectIntersectionOf@OWL2-RL
                                owl#SuperObjectComplementOf@OWL2-RL
                                owl#SuperObjectAllValuesFrom@OWL2-RL  owl#ObjectHasValue@OWL2-RL
                                owl#SuperObjectMaxCardinality@OWL2-RL owl#DataHasValue@OWL2-RL
                                owl#SuperDataMaxCardinality@OWL2-RL   owl#DataAllValuesFrom@OWL2-RL
                              } )
                       } )
             )
           }
           (owl#ClassExpression@OWL2-QL
             \. //partition { owl#ObjectClass_IRI owl#Restriction@OWL2-QL }
                partition
                { (owl#SubClassExpression@OWL2-QL
                    \. partition { owl#ObjectClass_IRI  owl#SubClassRestriction@OWL2-QL } )
                  (owl#SuperClassExpression@OWL2-QL
                    \. partition { owl#ObjectClass_IRI  owl#SuperClassRestriction@OWL2-QL })
                } )
           (owl#ClassExpression@OWL2-RL
             \. //partition { owl#ObjectClass_IRI  owl#Restriction@OWL2-RL }
                partition
                { (owl#SubClassExpression@OWL2-RL
                    \. partition { owl#ObjectClass_IRI_other_than_Thing
                                   owl#SubClassRestriction@OWL2-RL } )
                  (owl#SuperClassExpression@OWL2-RL
                    \. partition { owl#ObjectClass_IRI_other_than_Thing
                                   owl#SuperClassRestriction@OWL2-RL } )
                } )
      )
      (owl#DataRange = rdfs#Datatype, //in Turtle, "rdfs:Datatype" is used
         \. //see https://www.w3.org/TR/2012/REC-xmlschema11-2-20120405/#built-in-datatypes
            partition
            { (owl#Floating-point_number \. partition { xsd:float xsd:double })
              (owl#real = owl#real_ValueSpace,
                \. (owl#rational
                     \. (xsd#decimal
                          \. (xsd#integer
                               \. (xsd#long \. (xsd#int \. (xsd#short \. xsd#byte))) )
                             (xsd#nonNegativeInteger
                               \. xsd#positiveInteger
                                  (xsd#unsignedLong
                                    \. (xsd#unsignedInt
                                         \. (xsd#unsignedShort \. xsd#unsignedByte) ) ) )
                             (xsd#nonPositiveInteger \. xsd#negativeInteger) ) ) )
            }
            partition
            { (owl#Datatype_IRI = owl#Datatype)
              (owl#Anonymous_datatype /^ Anonymous_type,
               \. partition
                  { (owl#DataIntersectionOf
                      = ^(owl#Anonymous_datatype owl#intersectionOf=: .{2..* owl#DataRange}) )
                    (owl#DataUnionOf
                      = ^(owl#Anonymous_datatype owl#unionOf=: .{2..* owl#DataRange}) )
                    (owl#DataComplementOf
                      = ^(owl#Anonymous_datatype owl#complementOf=: 1 owl#DataRange) )
                    (owl#DataOneOf = ^(owl#Anonymous_datatype owl#oneOf=: .{1..* rdfs#Literal}),
                      \. (owl#DataOneOf1Literal 
                           = ^(owl#ClassExpression owl#oneOf=: .{1 rdfs#Literal}) ) )
                    (owl#DatatypeRestriction 
                      = ^(owl#Anonymous_datatype
                            owl#onDatatype =: 1 Datatype_IRI,
                            owl#withRestrictions: .{1..* owl#Datarange_restrictions} ) )
                 } )
            }
            (owl#DataRange@OWL2-EL 
              \. partition { ^(owl#real not /^^ xsd:nonPositiveInteger xsd#nonNegativeInteger) }
                 partition { owl#Datatype_IRI  owl#DataIntersectionOf@OWL2-EL 
                             owl#DataOneOf1Literal } )
            (owl#DataRange@OWL2-QL  //still no DataUnionOf
              \. partition { ^(owl#real not /^^ xsd:nonPositiveInteger xsd#nonNegativeInteger) }
                 partition { owl#Datatype_IRI  owl#DataIntersectionOf@OWL2-QL } )
            (owl#DataRange@OWL2-RL
              \. partition { owl#Floating-point_number  xsd#decimal }
                 partition { owl#Datatype_IRI  owl#DataIntersectionOf@OWL2-RL } )
      )
    };



Property_type@RDF = owl#PropertyExpressionOrChain,
 \. (rdf#Property \. rdfs#ContainerMembershipProperty)  
    partition
    { (owl#ObjectPropertyExpressionOrChain
        \. partition
           { (owl#ObjectPropertyExpression 
               \. partition
                  { (owl#InverseObjectProperty)
                    (owl#ObjectProperty = owl#ObjectProperty_IRI,
                       = owl#ObjectPropertyExpression@OWL2-EL )
                  } )
             (owl#PropertyExpressionChain = AND{ 2..* ObjectPropertyExpression })
           }
           partition
           { owl#SubObjectPropertyExpression
             owl#SuperObjectPropertyExpression 
           } )
      (owl#DataPropertyExpression
        \. (owl#DataProperty = owl#DataProperty_IRI) )
      (owl#AnnotationProperty = owl#AnnotationProperty_IRI,
        = rdfs#comment /*supertype of all RDFS annotation links*/ )
    };


    
   




r_relation@RDF ~[rdfs#Resource, rdfs#Resource]
 \.  (r_relation_from_or_to_AE-or-thing_that-should_be@RDF 
      \. partition
         { (r_relation_from_AE-or-thing_that-should_be@RDF
             \. r_relation_from_and_to_AE-or-thing_that-should_be@RDF //below
           )
           (r_relation_to_AE-or-thing_that-should_be@RDF
             \. r_relation_from_and_to_AE-or-thing_that-should_be@RDF //below
                (r_relation_to_value-or-thing-that-should-be@RDF \. rdf#value)
                (r_relation_to_CE-or-thing_that-should_be@RDFS
                  \. (rdfs#label ~[rdfs#Resource, rdfs#Literal]  /^ r_name) )
           )
         }
         r_relation_from_or_to_Type-or-thing_that-should_be@RDF //below
    )
    (owl#differentFrom ~[owl#Thing, owl#Thing] /^ r_different)
    (owl#sameAs ~[owl#Thing, owl#Thing] /^ r_equal)
    (r_annotation@RDFS
       \. (rdfs#comment \. r_annotation_without_link@OWL)
          (owl#annotationPropertyFromOntology ~[Document_IRI@OWL, owl#Thing]
            \. (owl#versionInfo /^ r_document_version)
               (owl#annotationPropertyBetweenOntologies ~[Document_IRI@OWL, Document_IRI@OWL]
                 \. (owl#incompatibleWith /^ r_incompatible_document)
                    (owl#priorVersion /^ r_incompatible_document)
                    (owl#backwardCompatibleWith /^ r_backward_compatible_document) )
          (rdfs#isDefinedBy /^ r_definition)
          rdfs#seeAlso   owl#deprecated ~[IRI, Boolean]
    );

    r_relation_from_and_to_AE-or-thing_that-should_be@RDF ~[rdfs#Resource, rdfs#Resource]
      \. r_relation_from_and_to_Type-or-thing_that-should_be@RDF  //below
         (r_relation_for_module_context@RDF
           \. r_namespace_definition@RDF ~[owl#Ontology,Namespace_shortcut_definition_in_context]
              owl#imports ~[owl#Ontology,Document_IRI@OWL] )
         (reification_relation@RDF ~[rdf#Statement, rdf#Resource]
           \. rdf#predicate@RDF  rdf#subject rdf#object
              owl#annotatedSource ~[owl#Axiom, owl#Class]
              owl#annotatedProperty ~[owl#Axiom, owl#Class]
              owl#annotatedTarget ~[owl#Axiom, owl#Class] )
         (r_relation_from_collection_to_AE-or-thing_that-should_be@RDF
           \. rdfs#r_member /* /^ r_member, //if from rdfs#Container; generalizes each rdf#_nnn 
                               /^^ rdfs#ContainerMembershipProperty */
              (r_relation_from_list@RDF ~[rdf#List, Thing]
                \. (rdf#first = r_first@RDF)  (rdf#rest = r_rest@RDF) ) );

    r_relation_from_or_to_type-or-thing_that-should_be@RDF ~[rdfs#Resource, rdfs#Resource]
        ~[rdfs#Resource, rdfs#Resource]
      \. (r_relation_from_Type-or-thing_that-should_be@RDF
           \. (r_relation_from_type@RDFS
                \. (r_relation_from_type_to_collection@RDF ~[Type@RDF,Collection]
                     \. owl#oneOf //to assert the "only" instances of the class
                        //DataOneOf in OWL/XML
                        owl#hasKey ~[owl#Class,.{1..* rdf#Property}] 
                        (r_relation_from_type_to_collection_of_types@RDF ~[Type,.{1..* Type@RDF}]
                          \. (rdf#r_relation_from_class_to_classes ~[owl#Class,.{1..* owl#Class}]
                               \. (owl#intersectionOf /^ r_types_intersection_of)
                                  (owl#unionOf /^ r_types_union_of) )
                             (rdf#r_relation_from_property_to_properties
                                 ~[rdf#Property,.{1..* rdf#Property}]
                               \. owl#propertyChainAxiom )
                             owl#withRestrictions ~[rdfs#Datatype, .{1..* rdfs#Datatype}]  )
                   )
                   (owl#r_relation_from_restriction ~[owl#Restriction,owl#Thing] 
                     /^ r_relation_from_anonymous_concept_type@OWL,
                     \. owl#onClass ~[owl#Restriction,owl#Class]
                        owl#onProperty  ~[owl#Restriction,rdf#Property]
                        (owl#onProperty_restriction 
                           \. owl#someValuesFrom ~[owl#Restriction, owl#ObjectPropertyExpression]
                              owl#allValuesFrom  ~[owl#Restriction, owl#ObjectPropertyExpression]
                              owl#hasValue ~[owl#Restriction, Individual]
                              owl#hasSelf ~[owl#Restriction, xsd#boolean] )
                        (owl#r_relation_from_restriction_to_nonNegativeInteger
                            ~[owl#Restriction,xsd#nonNegativeInteger]
                          /^ r_relation_from_anonymous_concept_type_to_value-token_type@OWL,
                          \. (owl#cardinality \. owl#qualifiedCardinality)
                             (owl#minCardinality ;\. owl#minQualifiedCardinality)
                             (owl#maxCardinality ;\. owl#maxQualifiedCardinality) )
                   )
                   (owl#r_relation_from_datatype ~[rdfs:Datatype,owl#Thing] 
                     \. (owl#r_relation_from_datatype_to_literal ~[rdfs:Datatype,rdfs#Literal] 
                          \. xsd#minInclusive  xsd#maxInclusive
                             xsd#minExclusive  xsd#maxExclusive ) ) 
              )
              (r_relation_from_and_to_type-or-thing_that-should_be@RDF
                \. (r_relation_from_and_to_Type@RDF
                     \. (r_relation_from_and_to_concept_type@RDFS ~[Class@RDFS, Class@RDFS]
                          \. r_relation_from_anonymous_concept_type_to_concept_type@OWL //above
                             (owl#equivalentClass = r_equivalent_concept_type@OWL)
                             (owl#complementOf = r_complement_type@OWL)
                             (rdfs#subClassOf ~[Class@RDFS, Class@RDFS] 
                               /^ r_super-or-equal_concept-type,
                               \. owl-dl#subClassOf ~[Class@OWL-DL, Class@OWL-DL] ) 
                             (r_relation_from_and_to_value-token_type@RDFS 
                                ~[rdfs#Datatype, rdfs#Datatype]
                               \. owl#datatypeComplementOf
                                  xsd#maxInclusive  xsd#maxInclusive )
                        )
                        (r_relation_from_relation_type_to_concept_type@RDFS
                            ~[rdf#Property, Class@RDFS]
                          \. (rdfs#domain /^ r_binary-relation-type_domain)
                             (rdfs#range /^ r_binary-relation-type_range) )
                        (r_relation_from_and_to_relation_type@RDFS ~[rdf#Property, rdf#Property]
                          \. (rdfs#subPropertyOf /^ r_super-or-equal_relation-type)
                             (owl#inverseOf /^ r_inverse )
                             (owl#propertyDisjointWith /^ r_disjoint_relation_type) )
                   ) )
         )
         (r_relation_to_type-or-thing_that-should_be@RDF
           \. (r_relation_to_type@RDFS ~[rdfs#Resource, Type@RDFS] 
                \. (rdf#type /^ r_type_or_equal) 
                   (rdf#datatype ~[rdfs#Literal, rdf#Datatype]  /^ r_datatype)
              )
         );