owl#Thing //has for subtype partition {sub#Individual sub#Type}: \. p{ //p{...} delimits a subtype partition, //e{...} delimits an incomplete set of exclusive subtypes (sub#Type = sub#Higher-order_type_instance, \. p{ rdf#Property (rdfs#Class \. owl#Class) } ) (sub#Non-type_thing = sub#First-order-type_instance, \. p{ sub#Individual (sub#Statement \. (rdf#Statement \. (owl#NegativePropertyAssertion .(?ns) := [?ns <=> [ [a rdf#statement ?s] [?ns <=> ! ?s] ]] ) ) (sub#Statement_with_only_one_relation = sub#relation) //Section 1.1 p{ sub#Anonymous_statement (sub#Named_statement \. (sub#Statement_named_via_rdfs-label = ^(sub#Statement rdfs#label: a owl#Thing) ) (sub#Statement_with_id = ^(sub#Statement sub#id: a owl#Thing)) ) } (Statement_for_inferences .(?p) :=> [a rdf#statement ?s <=> [?p => an owl#Thing] ] ) ) } (sub#Contextualization \. (sub#Contextualizing_value |. sub#False sub#True) ) ) }.

sub#relation .(*) \. p{ sub#non-binary_relation (sub#binary_relation = owl#topObjectProperty .(owl#Thing, owl#Thing)) //|^ rdf#Property } p{ owl#sameAs (owl#differentFrom \. p{ sub#different_but_equivalent sub#different_and_non-equivalent } ) } p{ (sub#equivalent = sub#"<==>", \. p{ (sub#equivalent_type, \. p{ (sub#equivalent_property = sub#eqP owl#equivalentProperty) (sub#equivalent_class = sub#eqC owl#equivalentClass) }) (sub#equivalent_non-type_thing \. p{ (sub#equivalent_statement .(sub#Statement, sub#Statement) = sub#"<=>") sub#equivalent_individual }) } p{ owl#sameAs sub#different_but_equivalent } ) (sub#non-equivalent = sub#"!<==>" \. (sub#non-equivalent_nor_entailing ! sub#extended-entailed_thing_or_equivalent, \. p{ (sub#non-equivalent_type .(sub#Type, sub#Type) \. p{ (sub#non-equivalent_property \. p{ owl#propertyDisjointWith (sub#non-equivalent_nor_exclusive_property = sub#neP) }) (sub#non-equivalent_class .(rdfs#Class, rdfs#Class) \. p{ owl#disjointWith (sub#non-equivalent_nor_exclusive_class = sub#not-disjoint_and_not-equivalent_class sub#neC) } (sub#non-equivalent_nor_subClassOf ! rdfs#subClassOf ) ) }) sub#non-equivalent_non-type_thing } //next type: the destination is a set and its members are not <==> to the source // nor to each other (sub#non-equivalent_things .(owl#Thing ?t, .{2..* owl#Thing} ?ts) = sub#neTs, := [ [?ts sub#member: ^t1 (^t2 != ^t1)] => [^t1 sub#non-equivalent: ^t2 ?t] ], \. p{ (sub#non-equivalent_exclusive_things :=> [ [?ts sub#member: ^t1 (^t2 != ^t1)] => [^t1 sub#exclusion: ^t2, ?t] ], \. (sub#counted-contextualizing-relation-types .(rdf:Statement, .{0..* rdf:Property}) \. sub#mandatory-contextualizing-relation-types ) ) (sub#non-equivalent_nor_exclusive_things .(owl#Thing ?t, .{2..* owl#Thing} ?ts) = sub#neTs, := [ [?ts sub#member: ^t1 (^t2 != ^t1)] => [^t1 sub#non-equivalent_nor_exclusive_thing: ^t2 ?t] ], \. p{ (sub#non-equivalent_nor_exclusive_types .(sub#Type, sub#Type) \. p{ (sub#non-equivalent_nor_exclusive_classes .(rdfs#Class, .{2..* rdfs#Class}) = sub#neCs) (sub#non-equivalent_nor_exclusive_properties .(rdf#Property, .{2..* rdf#Property}) = sub#nePs) }) sub#non-equivalent_nor_exclusive_non-types }) }) //each of the next subtypes is specialized in a next (sub-)section sub#strict_semantic_generalization_or_specialization sub#strict_extended_part_or_part-of sub#contextualizing-or-negating_relation ) ) } //each of the next subtypes is specialized in a next (sub-)section sub#definition_or_semantic_generalization_or_specialization_or_comparability sub#extended_part_or_part-of sub#relation_equivalent_to_a_CN_query .

sub#definition_or_semantic_generalization_or_specialization_or_comparability \. (sub#semantic_generalization_or_equivalent \. p{ sub#equivalent (sub#strict_semantic_generalization \. e{ (sub#type .(?, sub#Type) owl#inverseOf: sub#instance) sub#strict_extended-entailed_thing //specialized in the next subsection }) } c{ (sub#type_or_equivalent = rdf#type, //e.g. in Turtle: "owl:Class rdf:type owl:Class" \. p{ sub#equivalent_type sub#type } ) (sub#semantic_core-generalization_or_equivalent \. (sub#extended-entailed_thing_or_equivalent = sub#"==>", \. p{ sub#equivalent sub#strict_extended-entailed_thing } e{ (sub#supertype_or_equivalent = sub#supertype, \. p{ sub#equivalent_type sub#strict_supertype } p{ (sub#superProperty_or_equivalent = owl#subPropertyOf, \. p{ sub#equivalent_property sub#strict_superProperty } ) (sub#superClass_or_equivalent = rdfs#subClassOf, //e.g. in Turtle: owl:Class rdfs#subClassOf owl:Class \. p{ sub#equivalent_class sub#strict_superClass } ) } ) (sub#entailed_statement_or_equivalent = sub#"=>", \. p{ sub#equivalent_statement sub#strict_entailed_statement } sub#owl2_implication ) (sub#superIndividual_or_equivalent \. p{ sub#equivalent_individual sub#strict_superIndividual } ) })) }) (sub#semantic_specialization_or_equivalent owl#inverseOf: sub#semantic_generalization_or_equivalent, \. p{ sub#equivalent (sub#strict_semantic_specialization \. e{ (sub#instance owl#inverseOf: sub#type) sub#strict_extended-entailed-by_thing }) } (sub#semantic_core-specialization_or_equivalent owl#inverseOf: sub#semantic_core-generalization_or_equivalent, \. (sub#extended-entailed-by_thing_or_equivalent = sub#"<==", \. p{ sub#equivalent sub#strict_extended-entailed-by_thing } e{ (sub#entailed-by_statement_or_equivalent \. p{ sub#equivalent_statement sub#strict_entailed-by_statement } ) (sub#subIndividual_or_equivalent \. p{ sub#equivalent_individual sub#strict_subIndividual } ) (sub#subtype_or_equivalent = sub#subtype, owl#inverseOf: sub#supertype_or_equivalent, \. p{ sub#equivalent_type sub#strict_subtype } p{ (sub#subProperty_or_equivalent = sub#subProperty sub#superPropertyOf owl#inverseOf: sub#superProperty_or_equivalent, \. p{ sub#equivalent_property sub#strict_subProperty } ) (sub#subClass_or_equivalent = sub#subClass sub#superClassOf, owl#inverseOf: sub#superClass_or_equivalent, \. p{ sub#equivalent_class sub#strict_subClass } ) }) (sub#subtypes_or_equivalent-types .(sub#Type, .{2..* sub#Type ?t}) \. sub#strict_subtypes //details in next subsection (sub#complete_set_of_subtypes \. p{ (sub#complete_set_of_subClasses .(rdfs#Class, .{2..* rdfs#Class}) = sub#uoC owl#unionOf, \. sub#complete_set_of_strict_subClasses ) (sub#complete_set_of_subProperties = sub#uoP, \. sub#complete_set_of_strict_subProperties ) })) })) p{ sub#object_not_known_to_be_comparable_or_uncomparable_via_extended-entailment (sub#object_known_to_be_comparable_or_uncomparable_via_extended-entailment = sub#object_known_to_be_comparable_or_uncomparable, \. p{ (sub#comparable_via_extended-entailment \. p{ sub#equivalent sub#strict_generalization sub#strict_specialization } (sub#comparable_class .(rdfs#Class, rdfs#Class) //hence: \. p{ sub#equivalent_class sub#strict_superClass sub#strict_subClass } //or: \. p{ rdfs:subClassOf sub#strict_subClass) )) (sub#uncomparable_via_extended-entailment \. p{ sub#extended-entailment_exclusion (sub#known_to_be_uncomparable_but_not_exclusive_via_extended-entailment \. (sub#uncomparable-but-not-disjoint_type .(sub#Type, sub#Type) \. (sub#uncomparable-but-not-disjoint_class .(rdfs#Class, rdfs#Class) ! owl#disjointWith ) ) ) } p{ (sub#uncomparable_type .(sub#Type, sub#Type) \. (sub#uncomparable_class .(rdfs#Class, rdfs#Class) \. sub#uncomparable-but-not-disjoint_class ) ) sub#uncomparable_non-type }) } p{ (sub#type_known_to_be_comparable_or_uncomparable .(sub#Type, sub#Type) \. p{ (sub#class_known_to_be_comparable_or_uncomparable .(rdfs#Class, rdfs#Class) //hence: \. p{ sub#comparable_class sub#uncomparable_class } // or: \. p{ sub#comparable_class owl#disjointWith // sub#non-equivalent_class_nor_subClassOf } ) sub#property_known_to_be_comparable_or_uncomparable }) sub#non-type_known_to_be_comparable_or_uncomparable } ) } p{ sub#object_not_known_to_be_SUP-comparable-or-uncomparable_via_extended-entailment (sub#object_known_to_be_SUP-comparable-or-uncomparable_via_extended-entailment = sub#object_known_to_be_SUP-comparable_or_SUP-uncomparable, \. sub#object_known_to_be_comparable_or_uncomparable_via_extended-entailment p{ (sub#SUP-comparable_via_extended-entailment \. p{ sub#equivalent sub#strict_generalization } sub#comparable_via_extended-entailment (sub#SUP-comparable_class .(rdfs#Class, rdfs#Class) //hence: \. p{ sub#equivalent_class sub#strict_superClass } //or: = rdfs:subClassOf )) sub#not_known_to_be_SUP-comparable-or-uncomparable_via_extended-entailment (sub#SUP-uncomparable_via_extended-entailment \. p{ (sub#SUP-uncomparable_type .(sub#Type, sub#Type) \. (sub#SUP-uncomparable_class .(rdfs#Class, rdfs#Class) = sub#non-equivalent_class_nor_subClassOf \. sub#SUP-uncomparable-but-not-disjoint_class ) ) sub#SUP-uncomparable_non-type } sub#uncomparable_via_extended-entailment ) } p{ (sub#type_known_to_be_SUP-comparable-or-uncomparable .(sub#Type, sub#Type) \. p{ (sub#class_known_to_be_SUP-comparable-or-uncomparable .(rdfs#Class, rdfs#Class) = sub#class_known_to_be_SUP-comparable_or_exclusive_or_SUP-uncomparable //hence: \. p{ sub#comparable_class sub#uncomparable_class } // or: \. p{ sub#comparable_class owl#disjointWith // sub#non-equivalent_class_nor_subClassOf } ) sub#property_known_to_be_SUP-comparable-or-SUP-uncomparable }) sub#non-type_known_to_be_comparable_or_uncomparable } ) } (sub#definition \. c{ sub#"<==" sub#"==>" }, :=> "a full definition of a statement is equivalent to this statement" ).

sub#strict_generalization_or_specialization \. p{ (sub#strict_semantic_generalization \. (sub#strict_extended-entailed_thing \. e{ sub#strict_entailed_statement .(sub#Statement, sub#Statement) sub#strict_superIndividual .(sub#Individual, sub#Individual) (sub#strict_supertype .(sub#Type, sub#Type) \. p{ (sub#strict_superProperty .(rdf#Property, rdf#Property) = sub#proper-subPropertyOf ) (sub#strict_superClass = sub#proper-subClassOf) }) })) (sub#strict_semantic_specialization owl#inverseOf: sub#strict_generalization, \. (sub#strict_extended-entailed-by_thing \. e{ (sub#strict_entailed-by_statement .(sub#Statement, sub#Statement) owl#inverseOf: sub#strict_entailed_statement) (sub#strict_subIndividual owl#inverseOf: sub#strict_superIndividual) (sub#strict_subtype .(sub#Type, sub#Type) owl#inverseOf: sub#strict_supertype, \. p{ (sub#strict_subProperty .(rdf#Property, rdf#Property) = sub#proper-superPropertyOf, \. sub#sP sub#sP_ ) //although "sub#sP \. sub#sP_" is tempting //sP (sub#strict_subClass = sub#proper-subClass sub#proper-superClassOf, \. sub#sC sub#sC_ )//though "sub#sC \. sub#sC_" is tempting //sC } (sub#s .(sub#Type ?t, sub#Type ?st) := "strict subtype that is uncomparable but not disjoint to its siblings except for those which are connected by subtype relations or by exclusion relations (and hence already known to be non-equivalent)", := //the following definition use kif#"=>>" and kif#consis; see // "Knowledge Interchange Format, Version 3.0, Reference Manual" // (1992), pages 54-56, for their definitions; the FL parser // know these types [ [?t sub#strict-subtype: (^st2 != ?st)] => [kif#consis _([^st2 sub#uncomparable-but-not-disjoint_type ?st]) kif#=>> [^st2 sub#uncomparable-but-not-disjoint_type ?st] ] ], \. p{ sub#sP sub#sC } ) (sub#strict_subtype_uncomparable_but_not_disjoint_to_its_siblings .(sub#Type ?t, sub#Type ?st) = sub#s_, := //nearly as above but without requiring kif#consis and kif#=>> [ [?t sub#strict-subtype: (^st2 != ?st)] => [ [^st2 sub#uncomparable-but-not-disjoint_type ?st] => [^st2 sub#uncomparable-but-not-disjoint_type ?st] ] ], \. p{ (sub#sP_ .(rdf#Property, rdf#Property) = sub#sP_) (sub#sC_ = sub#proper-superClassOf_a-subclass-uncomparable-but-not-disjoint-with-its-siblings) }) ) }) (sub#strict_semantic_core_specializations \. (sub#strict_subtypes .(sub#Type ?t, .{2..* sub#Type ?st}) \. p{ (sub#strict_subProperties .(rdf#Property, .{2..* rdf#Property}) \. (sub#exclusive_strict_subProperties \. p{ (sub#property_partition = sub#pP) //pP (sub#incomplete_set_of_exclusive_subProperties = sub#eP) //eP }) (sub#complete_set_of_strict_subProperties \. p{ sub#property_partition (sub#complete_set_of_non-exclusive_strict_subProperties = sub#cP ) //cP }) ) (sub#strict_subClasses .(rdfs#Class, .{2..* rdfs#Class}) \. (sub#exclusive_strict_subClasses \. p{ (sub#class_partition = owl#disjointUnionOf sub#pP) //pC (sub#incomplete_set_of_exclusive_subClasses = sub#eC) //eC }) (sub#complete_set_of_strict_subClasses \. p{ sub#class_partition (sub#complete_set_of_non-exclusive_strict_subClasses = sub#cC ) //cC }) ) } e{ (sub#exclusive_strict_subtypes .(sub#Type ?t, .{2..* sub#Type}) = sub#eT, := [ [?t \. ^st1 (^st2 != ^st1)] => [^st1 sub#disjoint_type ^st2] ], \. p{ sub#exclusive_strict_subProperties sub#exclusive_strict_subClasses .(rdfs#Class, .{2..* rdfs#Class}) }) (sub#non-exclusive_strict_subtypes .(sub#Type ?t, .{2..* sub#Type}) := [ [?t \. ^st1 (^st2 != ^st1)] => [^st1 !sub#disjoint_type ^st2] ], \. p{ (sub#non-exclusive_strict_subProperties .(rdf#Property, .{2..* rdf#Property}) \. p{ sub#complete_set_of_non-exclusive_strict_subProperties sub#incomplete_set_of_non-exclusive_strict_subProperties }) (sub#non-exclusive_strict_subClasses .(rdfs#Class, .{2..* rdfs#Class}) \. p{ sub#complete_set_of_non-exclusive_strict_subClasses sub#incomplete_set_of_non-exclusive_strict_subClasses }) }) } p{ (sub#complete_set_of_strict_subtypes .(sub#Type ?t, .{2..* sub#Type} ?sTs) = sub#cT, := [ [?t \. ^st1] => [^st1 /^ (a sub#Type sub#member of: stTs)] ], \. p{ sub#complete_set_of_strict_subProperties sub#complete_set_of_strict_subClasses }) sub#incomplete_set_of_strict_subtypes } )) ) }.

sub#extended_part_or_part-of sub#type: owl#TransitiveProperty, \. p{ sub#equivalent sub#strict_extended_part_or_part-of } p{ sub#extended_part_or_part-of_directly_between_individuals .(sub#Individual, sub#Individual) (sub#extended_part_or_part-of_between_types_but_for_their_instances .(sub#Type, sub#Type) \. (sub#part_or_part-of_between_types_but_for_their_instances \. c{ sub#part_between_types_but_for_their_instances //see next subsection sub#part-of_between_types_but_for_their_instances //see next subsection })) } (sub#extended_part \. p{ sub#equivalent sub#strict_extended_part } e{ (sub#member_or_equivalent \. p{ sub#equivalent sub#member }) (sub#part_or_equivalent = sub#part, \. p{ sub#equivalent sub#strict_part }) (sub#c_part_or_equivalent \. p{ sub#eqC sub#c_part }) }) (sub#extended_part-of owl#inverseOf: sub#part-of_or_equivalent, \. p{ sub#equivalent sub#strict_extended_part-of } ) p{ sub#object_not_known_to_be_comparable-or-uncomparable_via_part (sub#object_known_to_be_comparable-or-uncomparable_via_part = sub#object_known_to_be_part-comparable-or-uncomparable, \. p{ (sub#comparable_via_part \. p{ owl#sameAs sub#part sub#part_of } ) (sub#uncomparable_via_part \. p{ sub#part_exclusion sub#part-uncomparable_but_not_part-exclusive }) }) } p{ sub#object_not_known_to_be_c_comparable-or-uncomparable_via_part (sub#object_known_to_be_c_comparable-or-uncomparable_via_part = sub#object_known_to_be_c_part-comparable-or-uncomparable, \. p{ (sub#comparable_via_c_part \. p{ sub#eqC sub#c_part sub#c_part_of } ) (sub#uncomparable_via_c_part \. p{ sub#c_part_exclusion sub#c_part-uncomparable_but_not_c_part-exclusive }) }) }.

sub#strict_extended_part_or_part-of \. (sub#strict_extended_part \. (sub#strict_part = sub#part, \. sub#sPart) (sub#part_between_types_but_for_their_instances .(sub#Type ?t1, sub#Type ?t2) = c_part, := [ [^i sub#type: ?t1] => [^i sub#part: a ?t2] ], \. c_sPart ) (sub#member .(owl#Thing, owl#Thing) \. (sub#statement_member .(sub#Statement, owl#Thing) \. (sub#definition_member \. sub#definition_member_via_OWL ) //see Section 3 //just another example: (sub#relation_member .(sub#Statement, owl#Thing) \. (sub#relation_type .(sub#Statement, owl#Thing) \. (sub#relation_type_of_an_RDF_reified_statement = rdf#predicate))))) (sub#"==>-element" = sub#extended-entailment_element, \. p{ (sub#"=>-element" .(sub#Statement ?X, sub#Statement ?y) = sub#entailment_element, := "∀X,y  =>-element(X,y) <=> (∃y2,Y (X=>Y) ∧ (Y <=> (y ∧ y2)))", := [?X => (a sub#Statement ?Y <=> [?y. (?y2 != ?y)])], \. (sub#"<=>-element" .(sub#Statement ?X, sub#Statement ?y) = sub#equivalent-statement_element, := [?X <=> [?y. (?y2 != ?y)] ] ) ) (sub#NC-definition_element .(owl#Thing ?t, owl#Thing ?e) := [?t sub#"==>": (a sub#Statement sub#statement_member: ?e)], \. (sub#NSC-definition_element .(owl#Thing ?t, owl#Thing ?e) := [?t <=> (a sub#Statement sub#statement_member: ?e)] ) ) }) (sub#"<==-element" = sub#extended-reverse-entailment_element, \. p{ (sub#"<=-element" .(sub#Statement ?X, sub#Statement ?y) = sub#reverse-entailment_element, := [?X <= (a sub#Statement ?Y <=> [?y. (?y2 != ?y)])], \. sub#"<=>-element" ) (sub#SC-definition_element .(owl#Thing ?t, owl#Thing ?e) := [?t sub#"<==": (a sub#Statement sub#statement_member: ?e)], \. sub#NSC-definition_element ) }) (sub#definition-element .(owl#Thing ?t, owl#Thing ?e) |^ owl#TransitiveProperty, \. c{ sub#NC-definition_element sub#SC-definition_element } p{ sub#def_necessary-element sub#def_non-necessary_element }, sub#definition-element_via_OWL //defined in Section 2 ) (sub#part-exclusive_parts .( sub#Individual ?i, .{2..* sub#Individual} ?pIs ) = sub#non-overlapping_parts, := [[?pIs sub#member: ^pI1 (^pI2 != ^pI1)] => [^pI1 sub#part_exclusion ^pI2]], \. p{ (sub#part_partition = sub#partPartition sub#pParts) //pParts (sub#incomplete_set_of_part-exclusive_parts = sub#eParts) //eParts }) (sub#c_part-exclusive_parts .( sub#Type ?t, .{2..* sub#Type} ?pTs ) := [ [^i sub#type: ?t, sub#part-exclusive_parts: ?pIs] [ [^pI sub#member of: ?pIs] => [^pI sub#type: (a sub#Type sub#member of: ?pTs)] ] ], \. p{ (sub#c_part_partition = sub#c_pParts) //c_pParts (sub#incomplete_set_of_part-exclusive_parts = sub#c_eParts) //c_eParts }) (sub#complete_set_of_parts .( sub#Individual ?i, .{2..* sub#Individual} ?pIs ) := [ [^e sub#part of: ?i] => [^e sub#part of: (a owl#Thing sub#member of: ?pIs)] ], \. p{ sub#part_partition (sub#complete_set_of_non-part-exclusive_parts = sub#cParts) //cParts }) (sub#c_complete_set_of_parts .( sub#Type ?t, .{2..* sub#Type} ?pTs ) := [ [^i sub#type: ?t, sub#union_of_parts: ?pIs] [ [^pI sub#member of: ?pIs] => [^pI sub#type: (a sub#Type sub#member of: ?pTs)] ] ], \. p{ sub#c_part_partition (sub#complete_set_of_c_non-part-exclusive_parts = sub#c_cParts) //c_cParts }) ) (sub#strict_extended_part-of \. (sub#strict_part-of = sub#part_of sub#partOf sub#superPart, owl#inverseOf: sub#strict_part) (sub#part-of_between_types_but_for_their_instances = sub#c_part_of sub#c_partOf, owl#inverseOf: sub#part_between_types_but_for_their_instances ) (sub#"elementOf-==>" = sub#elementOf-extended-entailment, \. p{ (sub#"elementOf-=>" .(sub#Statement ?x, sub#Statement ?Y) = sub#elementOf-entailment, := "∀x,Y  elementOf-=>(x,Y) <=> (∃X,x2!=x (X=>Y) ∧ (X <=> (x ∧ x2)))", := [a sub#Statement ?X => ?Y, <=> [?x. (?x2 != ?x)] ], \. (sub#"elementOf-<=>" .(sub#Statement ?x, sub#Statement ?Y) = sub#elementOf-equivalent-statement, := [?Y <=> [?x. (?x2 != ?x)] ] ) ) (sub#elementOf-NC-definition owl#inverseOf: sub#NC-definition-element) }) (sub#"elementOf-<==" = sub#elementOf-extended-reverse-entailment, \. p{ (sub#"elementOf-<=" .(sub#Statement ?x, sub#Statement ?Y) := [a sub#Statement ?X <= ?Y, <=> [?x. (?x2 != ?x)] ], \. sub#"elementOf-<=>" ) (sub#elementOf-SC-definition owl#inverseOf: sub#SC-definition-element) }) ).

sub#contextualizing-or-negating_relation \. p{ (sub#statement_contextualizing-or-negating_relation = sub#aboutness-relation \. (sub#statement_contextualizing-or-negating_binary-relation = sub#contextualization ) ) sub#non-statement_contextualizing-or-negating_relation } p{ (sub#pure_contextualizing_relation \. sub#time) (sub#extended_negation = sub#"!", \. p{ (sub#statement_negation = sub#negation) sub#non-statement_negation } //also derivable from signatures (sub#extended_exclusion \. (sub#extended-entailment_exclusion .(owl#Thing ?t1, owl#Thing ?t2) = sub#"==>!" sub#exclusion, sub#propertySymmetricNegation: sub#"==>",//so: //:= [ [ [^t sub#"==>": ?t1] => ![^t sub#"==>": ?t2] ] // [ [^t sub#"==>!" ?t2] => ![^t sub#"==>!": ?t1] ] ], \. e{ (sub#disjoint_type .(sub#Type, sub#Type) \. p{ (sub#disjoint_class = owl#disjointWith sub#disjC, \. owl#complementOf) (sub#disjoint_property .(rdf#Property, rdf#Property) = owl#propertyDisjointWith sub#disjP, \. (sub#propertySymmetricNegation .(?rt1, ?rt2) := [[[^x ?rt1: ^y]=>[ ![^x ?rt2: ^y] ![^y ?rt2: ^x]]] [[^x ?rt2: ^y]=>[ ![^x ?rt1: ^y] ![^y ?rt1: ^x]]]], \. sub#propertyFullExclusion ) ) }) sub#exclusive_non-type_thing }) (sub#propertySymmetricNegationOrExclusion .(?rt1, ?rt2) \. sub#propertySymmetricNegation (sub#propertySymmetricExclusion_of .(?rt1, ?rt2) := [ [^x ?rt1: ^y] <=> [ [[^e ?rt2: ^x] => ![^e ?rt2: ^y]] [[^e ?rt2: ^y] => ![^e ?rt2: ^x]] ] ], \. sub#propertyFullExclusion ) (sub#propertySymmetricExclusion_of .(?rt1, ?rt2) owl#inverseOf: sub#propertySymmetricExclusion \. sub#propertyFullExclusion ) ) (sub#extended-part_exclusion \. (sub#"==>-element_exclusion" = sub#extended-entailment-element_exclusion, sub#propertyFullExclusion of: sub#"==>-element", \. (sub#"==>-element_exclusion" sub#propertyFullExclusion of: sub#"==>-element", \. (sub#"<=>-element_exclusion" = sub#equivalent-statement-element_exclusion, sub#propertyFullExclusion of: sub#"<=>-element" ))) (sub#"<==-element_exclusion" = sub#extended-reverse-entailment-element_exclusion, sub#propertyFullExclusion of: sub#"<==-element", \. (sub#"<=-element_exclusion" sub#propertyFullExclusion of: sub#"<=-element", \. sub#"<=>-element_exclusion" )) (sub#definition-element_exclusion .(owl#Thing ?t1, owl#Thing ?t2) \. c{ (sub#NC-definition-element_exclusion sub#propertyFullExclusion of: sub#NC-definition-element ) (sub#SC-definition-element_exclusion sub#propertyFullExclusion of: sub#SC-definition-element ) } p{ (sub#def_necessary-element_exclusion sub#propertyFullExclusion of: sub#def_necessary-element ) (sub#def_non-necessary_element_exclusion sub#propertyFullExclusion of: sub#def_non-necessary_element ) }, sub#propertyFullExclusion: sub#definition-element ) (sub#part_exclusion .(sub#Individual ?i1, sub#Individual ?i2) = sub#part-disjointWith, sub#propertySymmetricNegation: sub#part, := "no shared part", := [no owl#Thing sub#part of: ?i1 ?i2], := [ [^e sub#part of: ^i1] => ![^e sub#part of: ^i2] [^e sub#part of: ^i2] => ![^e sub#part of: ^i1] ] ) (sub#c_part_exclusion .(sub#Type ?t1, sub#Type ?t2) , sub#propertySymmetricNegation: sub#c_part, := [ [ [^i1 sub#type: ?t1] [^i2 sub#type: ?t2] ] => [^i1 sub#part_exclusion: ^i2] ] ) ) (sub#extended-part-of_exclusion \. (sub#"elementOf-<==_exclusion" sub#propertyFullExclusion of: sub#"elementOf-<==" ) (sub#"elementOf-=>_exclusion" sub#propertyFullExclusion of: sub#"elementOf-==>" ) ) (sub#type_exclusion .(owl#Thing ?t1, owl#Thing ?t2) sub#propertyFullExclusion of: sub#type_or_equivalent ) /* negation: ![?t1 type: ?t2], ![?t2 type: ?t1] exclusion: [ [ [^i sub#type: ?t1] => ![^i sub#type: ?t2] ] [ [^i sub#type: ?t2] => ![^i sub#type: ?t1] ] ] */ )) }.

sub#definition_element_via_OWL \. p{ sub#class-definition_element sub#datatype-definition_element sub#property-definition_element (sub#instance-definition_element \. sub#instance owl#hasKey) }. sub#class-definition_element \. sub#proper-superClassOf owl#complementOf (sub#class-def_union_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#unionOf: ?p)] ) (sub#class-def_intersection_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#intersectionOf: ?p)] ) (sub#class-def_onProperty_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#onProperty: ?p)] ) (sub#class-def_onClass_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#onClass: ?p)] ) (sub#class-def_someValuesFrom_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#someValuesFrom: ?p)] ) (sub#class-def_allValuesFrom_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#allValuesFrom: ?p)] ) (sub#class-def_hasValue_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#hasValue: ?p)] ) (sub#class-def_hasSelf_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#hasSelf: ?p)] ) (sub#class-def_oneOf_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#oneOf: ?p)] ) (sub#class-def_cardinality_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#cardinality: ?p)] ) (sub#class-def_minCardinality_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#minCardinality: ?p)] ) (sub#class-def_maxCardinality_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#maxCardinality: ?p)] ) (sub#class-def_qCardinality_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#qualifiedCardinality: ?p)] ) (sub#class-def_maxCard_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#minQualifiedCardinality: ?p)] ) (sub#class-def_minCard_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#maxQualifiedCardinality: ?p)] ). sub#datatype-definition_element \. (sub#datatype-def_minRestr_part .(?t, ?p) := [?t owl#withRestrictions: (a owl#Thing xsd#minInclusive : ?p)] ) (sub#datatype-def_maxRestr_part .(?t, ?p) := [?t rdfs#subClassOf: (a owl#Thing owl#unionOf: ?p)] ). sub#property-definition_element \. sub#proper-superPropertyOf owl#inverseOf rdfs#domain rdfs#range (sub#propertyChainAxiom_member \. (sub#chain_member1 .(?t, ?p) := [?t owl#propertyChainAxiom: (a owl#Thing rdf#first: ?p)] ) (sub#chain_member2 .(?t, ?p) := [?t owl#propertyChainAxiom: (a owl#Thing rdf#rest: (a owl#Thing rdf#first: ?p))]) (sub#chain_member3 .(?t, ?p) := [?t owl#propertyChainAxiom: (a owl#Thing rdf#rest: (a owl#Thing rdf#rest: (a owl#Thing rdf#first: ?p)))] )). //and so on, as many as needed

/* With the notation used in the article: - CN({every owl:Thing}, {==>, <==>}) checks that every object in the evaluated KB is sub:object_known_to_be_comparable_or_uncomparable to every object in this KB. - CN({every rdfs:Class}, {rdfs:subClassOf, owl:equivalentClass, owl:sameAs}) checks that every class in the KB is sub#class_known_to_be_comparable_or_uncomparable to every object in this KB. - CN({every owl:Thing}, {==>, <==>},{"every object to some other object"}) checks that every object is sub:object_known_to_be_SUP-comparable-or-SUP-uncomparable to some other object in this KB. - CN({every rdfs:Class}, {rdfs:subClassOf, owl:equivalentClass, owl:sameAs}, {"every object to some other object"}) checks that every class is sub:class_known_to_be_SUP-comparable-or-SUP-uncomparable some other object in this KB. */