Top Engine Code
Status: Alpha
Brought to you by:
topengine
Menu
▾
▴
[r12]: / trunk / py_top_module / top / owl-reasoner.trd Maximize Restore History
1519 lines (1254 with data), 66.8 kB
############################################################################
# owl-reasoner.trd
#
############################################################################
############################################################################
# include section
#
# Include the meta meta model which defines the owl: and rdf: resources
# name that may be used in this file.
############################################################################
# *MD Omitted the included due to path issue when deployed with apache (defect)
# *include-file* "top/meta_meta_model.trd"
############################################################################
# schema section
#
# *MD File top/meta_meta_model.trd included here to avoid to use the include directive
############################################################################
*schema-begin*
#
# owl namespace
#
owl:AllDifferent = resource("owl:AllDifferent")
owl:AnnotationProperty = resource("owl:AnnotationProperty")
owl:Class = resource("owl:Class")
owl:DataRange = resource("owl:DataRange")
owl:DeprecatedClass = resource("owl:DeprecatedClass")
owl:DeprecatedProperty = resource("owl:DeprecatedProperty")
owl:DatatypeProperty = resource("owl:DatatypeProperty")
owl:FunctionalProperty = resource("owl:FunctionalProperty")
owl:InverseFunctionalProperty = resource("owl:InverseFunctionalProperty")
owl:Nothing = resource("owl:Nothing")
owl:ObjectProperty = resource("owl:ObjectProperty")
owl:Ontology = resource("owl:Ontology")
owl:OntologyProperty = resource("owl:OntologyProperty")
owl:Restriction = resource("owl:Restriction")
owl:SymmetricProperty = resource("owl:SymmetricProperty")
owl:Thing = resource("owl:Thing")
owl:TransitiveProperty = resource("owl:TransitiveProperty")
owl:allValuesFrom = resource("owl:allValuesFrom")
owl:backwardCompatibleWith = resource("owl:backwardCompatibleWith")
owl:cardinality = resource("owl:cardinality")
owl:complementOf = resource("owl:complementOf")
owl:differentFrom = resource("owl:differentFrom")
owl:disjointWith = resource("owl:disjointWith")
owl:distinctMembers = resource("owl:distinctMembers")
owl:equivalentClass = resource("owl:equivalentClass")
owl:equivalentProperty = resource("owl:equivalentProperty")
owl:hasValue = resource("owl:hasValue")
owl:imports = resource("owl:imports")
owl:incompatibleWith = resource("owl:incompatibleWith")
owl:intersectionOf = resource("owl:intersectionOf")
owl:inverseOf = resource("owl:inverseOf")
owl:maxCardinality = resource("owl:maxCardinality")
owl:minCardinality = resource("owl:minCardinality")
owl:onProperty = resource("owl:onProperty")
owl:oneOf = resource("owl:oneOf")
owl:priorVersion = resource("owl:priorVersion")
owl:sameAs = resource("owl:sameAs")
owl:someValuesFrom = resource("owl:someValuesFrom")
owl:unionOf = resource("owl:unionOf")
owl:versionInfo = resource("owl:versionInfo")
#
# rdf/rdfs namespace
#
rdf:Description = resource("rdf:Description")
rdf:Property = resource("rdf:Property")
rdf:type = resource("rdf:type")
rdfs:Class = resource("rdfs:Class")
rdfs:Datatype = resource("rdfs:Datatype")
rdfs:comment = resource("rdfs:comment")
rdfs:domain = resource("rdfs:domain")
rdfs:range = resource("rdfs:range")
rdfs:subClassOf = resource("rdfs:subClassOf")
rdfs:subPropertyOf = resource("rdfs:subPropertyOf")
#
# top namespace
#
top:cardinality_gate = resource("top:cardinality_gate")
top:consistent_on = resource("top:consistent_on")
top:distinct = resource("top:distinct")
top:inherited_sub_class_of = resource("top:inherited_sub_class_of")
top:invalid_property = resource("top:invalid_property")
top:invalid_transitive_property = resource("top:invalid_transitive_property")
top:is_domain_class = resource("top:is_domain_class")
top:label = resource("top:label")
top:not_all_value_on = resource("top:not_all_value_on")
top:not_empty_set = resource("top:not_empty_set")
top:not_subset_of = resource("top:not_subset_of")
top:propertyError = resource("top:propertyError")
top:same_as = resource("top:same_as")
xsd:float = resource("xsd:float")
true = bool("true")
false = bool("false")
*schema-end*
############################################################################
############################################################################
# knowledge base section
#
############################################################################
*knowledge-base-begin*
default-explain = true
default-optimization = true
default-lookup-index = true
max-rule-visit = 50000
*knowledge-base-end*
############################################################################
############################################################################
# knowledge rules section
#
############################################################################
*knowledge-rules-begin*
# ///////////////////////////////////////////////////////////////////
# LOGICAL CONSEQUENCES APPLICABLE TO CLASSES.
# ///////////////////////////////////////////////////////////////////
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# rdfs:subClassOf
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# rdfs:subClassOf is transitive: (A < B) and (B < C) => (A < C)
#
[n=rule_inherited_base_class2, s=100]: \
(?c1 rdfs:subClassOf ?c2). \
(?c2 rdfs:subClassOf ?c3). \
[?c1 different_from ?c3] \
-> \
(?c1 rdfs:subClassOf ?c3)
#
# Ensure all classes (owl:Class) are rdfs:subClassOf owl:Thing.
#
[n=rule_sub_class_thing, s=80]: \
(?c1 rdf:type owl:Class). \
[((?c1 different_from owl:Thing) and \
(?c1 exist_not rdfs:subClassOf))] \
-> \
(?c1 rdfs:subClassOf owl:Thing)
#
# Ensure all owl:Restriction are rdfs:subClassOf owl:Thing.
#
[n=rule_class_restriction, s=100]: \
(?c1 rdf:type owl:Restriction) \
-> \
(?c1 rdfs:subClassOf owl:Thing)
#
# In OWL DL an individual can never be at the same time a class:
# classes and individuals form disjoint domains.
#
[n=err_rule_individuals_and_classes, s=100]: \
(?c2 rdf:type owl:Class). \
(?s1 rdf:type owl:Class). \
(?s1 rdf:type ?c2) \
-> \
(?s1 rdf:type owl:Nothing)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:equivalentClass
#
# Note: owl:equivalentClass is asserted rather than inferred.
# The basic construct is owl:subClassOf.
# Do not infer owl:equivalentClass from classes that are mutually
# owl:subClassOf each other this would lead to cycling for inconsistent
# models.
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# owl:equivalentClass is symetric: (A = B) => (B = A)
#
[n=rule_symetry_of_equ_class, s=100]: \
(?c1 owl:equivalentClass ?c2) \
-> \
(?c2 owl:equivalentClass ?c1)
#
# owl:equivalentClass is transitive: (A = B) ^ (B = C) => (A = C)
#
[n=rule_trans_of_equ_class, s=100]: \
(?c1 owl:equivalentClass ?c2). \
(?c2 owl:equivalentClass ?c3). \
[(?c1 different_from ?c3)] \
-> \
(?c1 owl:equivalentClass ?c3)
#
# owl:equivalentClass subsume each other: (A = B) => (A < B) and (B < A)
#
[n=rule_subsume_equ_class, s=100]: \
(?c1 owl:equivalentClass ?c2) \
-> \
(?c1 rdfs:subClassOf ?c2)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:intersectionOf
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# owl:intersectionOf is used in covering axiom:
# (A = (B ^ C)) => (A < B) and (A < C)
#
[n=rule_intersect_axiom1, s=100]: \
(?c1 owl:intersectionOf ?c2) \
-> \
(?c1 rdfs:subClassOf ?c2)
#
# Determine that a class is a subset of a class defined by the
# conjuction of some of it's base classes:
# (A = (A1 ^ A2...An)) and (B < A1) ... (B < An) => (B < A)
#
# This rule determine the sets that are different.
#
[n=rule_intersect_axiom2, s=95, o=f]: \
(?A owl:intersectionOf ?A1). \
(?B rdfs:subClassOf ?A1). \
[?A different_from ?B]. \
(?A owl:intersectionOf ?A2). \
[?A1 different_from ?A2]. \
not(?B rdfs:subClassOf ?A2) \
-> \
(?B top:not_subset_of ?A)
#
# Determine that a class is a subset of a class defined by the
# conjuction of some of it's base classes:
# (A = (A1 ^ A2...An)) and (B < A1) ... (B < An) => (B < A)
#
# Assume that (B < A) unless proven otherwise.
#
[n=rule_intersect_axiom3, s=85, o=f]: \
(?A owl:intersectionOf ?A1). \
(?B rdfs:subClassOf ?A1). \
[?A different_from ?B)]. \
not(?B top:not_subset_of ?A) \
-> \
(?B rdfs:subClassOf ?A)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:unionOf
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# owl:unionOf is used in covering axiom.
# (A = (B | C)) => (B < A) and (C < A)
#
[n=rule_union_axiom1, s=100]: \
(?c1 owl:unionOf ?c2) \
-> \
(?c2 rdfs:subClassOf ?c1)
#
# A disjuction of classes contained in a disjuction of a greater
# number of classes is a subset:
# (A = (A1 | A2...An)) and (B = (A1 | A2...Am)) and (m <= n) => (B < A)
#
# This rule proves that (B = (A1 | A2...Am)) does not hold;
# i.e., that A does not have all classes in the union of B.
#
[n=rule_union_axiom2, s=110]: \
(?B owl:unionOf ?a1). \
(?A rdf:type owl:Class). \
[(?A different_from ?B) and (?A exist owl:unionOf)]. \
not(?A owl:unionOf ?a1) \
-> \
(?B top:not_subset_of ?A)
#
# A disjuction of classes contained in a disjuction of a greater
# number of classes is a subset:
# (A = (A1 | A2...An)) and (B = (A1 | A2...Am)) and (m <= n) => (B < A)
#
# Assume (B < A) unless proven otherwise.
#
[n=rule_union_axiom3, s=90]: \
(?A rdf:type owl:Class). \
[?A exist owl:unionOf]. \
(?B rdf:type owl:Class). \
[(?A different_from ?B) and (?B exist owl:unionOf)]. \
not(?B top:not_subset_of ?A) \
-> \
(?B rdfs:subClassOf ?A)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:disjointWith
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# owl:disjointWith is symetric: (A != B) => (B != A)
#
[n=rule_symetry_of_disjoint_class, s=100]: \
(?A owl:disjointWith ?B) \
-> \
(?B owl:disjointWith ?A)
#
# A class is disjoint with subclasses of it's disjoint class:
# (A != B) and (C < B) => (A != C)
#
[n=rule_disjoint_class1, s=100]: \
(?A owl:disjointWith ?B). \
(?C rdfs:subClassOf ?B) \
-> \
(?A owl:disjointWith ?C)
#
# Subclasses of disjoint classes are disjoint:
# (A != B) and (C < A) and (D < B) => (C != D)
#
[n=rule_disjoint_class2, s=100]: \
(?A owl:disjointWith ?B). \
(?C rdfs:subClassOf ?A). \
(?D rdfs:subClassOf ?B) \
-> \
(?C owl:disjointWith ?D)
#
# A class subclass of 2 disjoint classes is owl:Nothing:
# (A < B) and (A < C) and (B != C) => (A < 0)
#
[n=err_rule_sub_class_of_disjoint_classes, s=100]: \
(?A rdfs:subClassOf ?B). \
(?A rdfs:subClassOf ?C). \
[?B different_from ?C]. \
(?B owl:disjointWith ?C) \
-> \
(?A rdfs:subClassOf owl:Nothing)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:complementOf
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# owl:complementOf is symetric: (A ~= B) => (B ~= A)
#
[n=rule_complement_class1, s=100]: \
(?A owl:complementOf ?B) \
-> \
(?B owl:complementOf ?A)
#
# Complement classes are disjoint: (A ~= B) => (A != B)
#
[n=rule_complement_class2, s=100]: \
(?A owl:complementOf ?B) \
-> \
(?A owl:disjointWith ?B)
#
# A class can have only one complement class:
# (A ~= B) and (B ~= C) => (A = C)
#
[n=rule_complement_class3, s=100]: \
(?A owl:complementOf ?B). \
(?B owl:complementOf ?C). \
[?A different_from ?C] \
-> \
(?A owl:equivalentClass ?C)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:oneOf
# (used for class expression as enumerated set.)
#
# owl:oneOf is used in covering axiom where all possible
# individuals are named.
#
# Set A subsume set B if all individuals in set B are included in set A.
# This consider individuals that are equivalents (owl:sameAs)
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# Individuals that are equivalent are in same enumerated sets:
# (a < A) and (a = b) => (b < A)
#
[n=rule_oneof_util1, s=120]: \
(?c1 owl:oneOf ?o1). \
(?o1 owl:sameAs ?o2) \
-> \
(?c1 owl:oneOf ?o2)
#
# An enumerated class not the subset of it's super-class must
# be empty:
# (A < B) and (a1 < A) and not(a1 < B) => (A < 0)
#
#
[n=err_rule_oneof_axiom4, s=100]: \
(?A rdfs:subClassOf ?B). \
(?A top:not_subset_of ?B) \
-> \
(?A rdfs:subClassOf owl:Nothing)
#
# Empty enumerated set must have it's enumerated individuals
# of type Nothing:
# (A < 0) and (a1 < A) => (a1 < 0)
#
#
[n=err_rule_oneof_axiom5, s=100]: \
(?A rdfs:subClassOf owl:Nothing). \
(?A owl:oneOf ?a1) \
-> \
(?a1 rdf:type owl:Nothing)
#
# This rule determine the sets that are different.
#
[n=rule_oneof_axiom1, s=105]: \
(?c1 owl:oneOf ?o1). \
(?c2 rdf:type owl:Class). \
[(?c1 different_from ?c2) and (?c2 exist owl:oneOf)]. \
not(?c2 owl:oneOf ?o1) \
-> \
(?c1 top:not_subset_of ?c2)
#
# Assume sets having oneOf construct are equivalent by default.
# The rule above will prove otherwise if needed.
# all(a < A) and (a < B) => (A < B)
#
[n=rule_oneof_axiom2, s=100]: \
(?c1 rdf:type owl:Class). \
[?c1 exist owl:oneOf]. \
(?c2 rdf:type owl:Class). \
[(?c1 different_from ?c2) and (?c2 exist owl:oneOf)]. \
not(?c1 top:not_subset_of ?c2) \
-> \
(?c1 rdfs:subClassOf ?c2)
#
# Two sets known to be equivalent must have their members
# pair-wise equivalent unless known to be different.
# (A = B) and (a < A) and (b < B) and not(a != b) => (a = b)
#
[n=rule_oneof_axiom3, s=110]: \
(?c1 owl:oneOf ?o1). \
(?c2 owl:oneOf ?o2). \
[(?c1 different_from ?c2) and (?o1 different_from ?o2)]. \
(?c1 owl:equivalentClass ?c2). \
not(?o1 owl:differentFrom ?o2). \
not(?c1 top:not_subset_of ?c2) \
-> \
(?o1 owl:sameAs ?o2)
# ///////////////////////////////////////////////////////////////////
# Sets with all members of rdf:type owl:Nothing are empty.
# Empty sets extend owl:Nothing.
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# Rule to identify sets that are not empty.
#
[n=rule_not_empty_set, s=40]: \
(?c1 owl:oneOf ?o1). \
not(?o1 rdf:type owl:Nothing) \
-> \
(?c1 top:not_empty_set true)
#
# Assume enumerated sets to be empty unless proof of otherwise.
#
[n=err_rule_empty_set, s=30]: \
(?c1 rdf:type owl:Class). \
[?c1 exist owl:oneOf]. \
not(?c1 top:not_empty_set true) \
-> \
(?c1 rdfs:subClassOf owl:Nothing)
# ///////////////////////////////////////////////////////////////////
# LOGICAL CONSEQUENCES APPLICABLE TO INDIVIDUALS.
# ///////////////////////////////////////////////////////////////////
# ///////////////////////////////////////////////////////////////////
# Infer class membership of individuals based on class hierarchy.
#
# This applies to individuals.
# ///////////////////////////////////////////////////////////////////
#
# Individuals must have rdf:type as specified by class hierarchy:
# (a < A) and (A < B) => (a < B)
#
[n=rule_ind_membership1, s=50]: \
(?s1 rdf:type ?c1). \
(?c1 rdfs:subClassOf ?c2) \
-> \
(?s1 rdf:type ?c2)
#
# Individuals member of two classes that are disjoint must be owl:Nothing:
# (a < A) and (a < B) and (A != B) => (a < 0)
#
[n=err_rule_ind_membership2, s=50]: \
(?s1 rdf:type ?c1). \
(?s1 rdf:type ?c2). \
[?c1 different_from ?c2]. \
(?c1 owl:disjointWith ?c2) \
-> \
(?s1 rdf:type owl:Nothing)
#
# Individual can only be same and different from another one if it is owl:Nothing:
# (a = b) and (a != b) => (a < 0)
#
[n=err_rule_ind_membership3, s=50]: \
(?a owl:sameAs ?b). \
(?a owl:differentFrom ?b). \
[?a different_from ?b] \
-> \
(?a rdf:type owl:Nothing)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:sameAs
#
# owl:sameAs is used for constructing enumerated sets.
# This applies to individuals.
# ///////////////////////////////////////////////////////////////////
#
# owl:sameAs is symetric: (a = b) => (b = a)
#
[n=rule_symetry_of_same_as, s=120]: \
(?s1 owl:sameAs ?s2) \
-> \
(?s2 owl:sameAs ?s1)
#
# owl:sameAs is transitive: (a = b) and (b = c) => (a = c)
#
[n=rule_trans_of_same_as, s=120]: \
(?s1 owl:sameAs ?s2). \
(?s2 owl:sameAs ?s3). \
[?s1 different_from ?s3] \
-> \
(?s1 owl:sameAs ?s3)
#
# owl:sameAs individuals have same type:
# (a = b) and (a < A) => (b < A)
#
[n=rule_same_as_type1, s=100]: \
(?a owl:sameAs ?b). \
(?a rdf:type ?A) \
-> \
(?b rdf:type ?A)
#
# SameAs individuals participate in same relations:
# (x = y) and P(x, z) => P(y, z)
#
[n=rule_same_prop1, s=100]: \
(?p rdfs:subClassOf rdf:Property). \
(?x owl:sameAs ?y). \
(?x ?p ?z). \
[?z different_from ?y] \
-> \
(?y ?p ?z)
#
# SameAs individuals participate in same relations:
# (z = z1) and P(x, z) => P(x, z1)
#
[n=rule_same_prop2, s=100]: \
(?p rdfs:subClassOf rdf:Property). \
(?z owl:sameAs ?z1). \
(?x ?p ?z). \
[?x different_from ?z1] \
-> \
(?x ?p ?z1)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:differentFrom
#
# owl:differentFrom is used for constructing enumerated sets.
# This applies to individuals.
# ///////////////////////////////////////////////////////////////////
#
# owl:differentFrom is symetric: (a != b) => (b != a)
#
[n=rule_symetry_of_different_from, s=120]: \
(?s1 owl:differentFrom ?s2) \
-> \
(?s2 owl:differentFrom ?s1)
#
# Same individuals have common different individuals:
# (a = b) and (b != c) => (a != c)
#
[n=rule_trans_of_different_from, s=120]: \
(?a owl:sameAs ?b). \
(?b owl:differentFrom ?c). \
[?a different_from ?c] \
-> \
(?a owl:differentFrom ?c)
#
# owl:distinctMembers is syntactic sugar to owl:differentFrom
#
[n=rule_distinct_memb_axiom, s=120]: \
(?c1 owl:distinctMembers ?s1). \
(?c1 owl:distinctMembers ?s2). \
[?s1 different_from ?s2] \
-> \
(?s1 owl:differentFrom ?s2)
# ///////////////////////////////////////////////////////////////////
# LOGICAL CONSEQUENCES APPLICABLE TO PROPERTIES.
# ///////////////////////////////////////////////////////////////////
#
# Detect error in property semantic
#
[n=rule_err_prop1, s=100]: \
(?p1 rdf:type owl:DatatypeProperty). \
(?p1 rdf:type owl:ObjectProperty) \
-> \
(?p1 top:propertyError top:invalid_property)
#
# Detect error in property range
#
[n=rule_err_prop_disjoint_range1, s=100]: \
(?p1 rdfs:range ?c1). \
(?p1 rdfs:range ?c2). \
[?c1 different_from ?c2]. \
(?c1 owl:disjointWith ?c2) \
-> \
(?p1 top:propertyError top:invalid_property)
#
# Detect error in property domain
#
[n=rule_err_prop_disjoint_domain1, s=100]: \
(?p1 rdfs:domain ?c1). \
(?p1 rdfs:domain ?c2). \
[?c1 different_from ?c2]. \
(?c1 owl:disjointWith ?c2) \
-> \
(?p1 top:propertyError top:invalid_property)
# ///////////////////////////////////////////////////////////////////
# Ensure to have both owl:ObjectProperty and owl:DatatypeProperty
# subclasses of the RDF class rdf:Property.
#
# This applies to properties.
# ///////////////////////////////////////////////////////////////////
#
[n=rule_prop1, s=120]: \
(?p1 rdf:type owl:ObjectProperty) \
-> \
(?p1 rdfs:subClassOf rdf:Property)
[n=rule_prop2, s=120]: \
(?p1 rdf:type owl:DatatypeProperty) \
-> \
(?p1 rdfs:subClassOf rdf:Property)
#
# Subject must be of type specified by the property domain:
# P(x, y) and (P domain C) => (x < C)
#
[n=rule_prop3, s=120]: \
(?s ?p ?o). \
(?p rdfs:domain ?d) \
-> \
(?s rdf:type ?d)
#
# Object must be of type specified by the property range:
# P(x, y) and (P range C) => (y < C)
#
[n=rule_prop4, s=120]: \
(?s ?p ?o). \
(?p rdfs:range ?d) \
-> \
(?o rdf:type ?d)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# rdfs:subPropertyOf
#
# This applies to properties.
# ///////////////////////////////////////////////////////////////////
#
# In OWL DL the subject and object of a subproperty (rdfs:subPropertyOf) statement must be either both
# datatype properties or both object properties.
#
[n=rule_sub_prop11, s=120]: \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 rdf:type owl:ObjectProperty) \
-> \
(?p1 rdf:type owl:ObjectProperty)
[n=rule_sub_prop12, s=120]: \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 rdf:type owl:DatatypeProperty) \
-> \
(?p1 rdf:type owl:DatatypeProperty)
#
# rdfs:subPropertyOf have domain of parent property
# Subproperty must have sub-domain parent property:
# (P1 < P2) and (P1 domain C1) and (P2 domain C2) => (P1 domain (C1 ^ C2))
#
[n=rule_sub_prop2, s=120]: \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 rdfs:domain ?d) \
-> \
(?p1 rdfs:domain ?d)
#
# rdfs:subPropertyOf have range of parent property
# Subproperty must have sub-range of parent property:
# (P1 < P2) and (P1 range C1) and (P2 range C2) => (P1 range (C1 ^ C2))
#
[n=rule_sub_prop3, s=120]: \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 rdfs:range ?d) \
-> \
(?p1 rdfs:range ?d)
#
# Transitivity of subproperty relation: (P1 < P2) and (P2 < P3) => (P1 < P3)
#
[n=rule_sub_prop4, s=120]: \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 rdfs:subPropertyOf ?p3). \
[?p1 different_from ?p3] \
-> \
(?p1 rdfs:subPropertyOf ?p3)
[n=rule_sub_prop5, s=120]: \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 top:propertyError ?x) \
-> \
(?p1 top:propertyError ?x)
#
# Inheritance of properties: P1(x, y) and (P1 < P2) => P2(x, y)
#
[n=rule_sub_prop6, s=100]: \
(?p1 rdfs:subPropertyOf ?p2). \
(?x ?p1 ?y) \
-> \
(?x ?p2 ?y)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:equivalentProperty
#
# This applies to properties.
# ///////////////////////////////////////////////////////////////////
#
# owl:equivalentProperty is symetric
#
[n=rule_sym_equivalent_prop1, s=120]: \
(?p1 owl:equivalentProperty ?p2) \
-> \
(?p2 owl:equivalentProperty ?p1)
#
# owl:equivalentProperty is transitive
#
[n=rule_trans_equivalent_prop1, s=120]: \
(?p1 owl:equivalentProperty ?p2). \
(?p2 owl:equivalentProperty ?p3). \
[?p1 different_from ?p3] \
-> \
(?p1 owl:equivalentProperty ?p3)
#
# owl:equivalentProperty have same domain
#
[n=rule_domain_equivalent_prop1, s=120]: \
(?p1 owl:equivalentProperty ?p2). \
(?p2 rdfs:domain ?d) \
-> \
(?p1 rdfs:domain ?d)
#
# owl:equivalentProperty have same range
#
[n=rule_range_equivalent_prop1, s=120]: \
(?p1 owl:equivalentProperty ?p2). \
(?p2 rdfs:range ?d) \
-> \
(?p1 rdfs:range ?d)
#
# owl:equivalentProperty have same "property extension"
# (P1 = P2) => (P1 < P2) and (P2 < P1)
#
[n=rule_equivalent_prop1, s=120]: \
(?P1 owl:equivalentProperty ?P2) \
-> \
(?P1 rdfs:subPropertyOf ?P2). \
(?P2 rdfs:subPropertyOf ?P1)
#
# owl:equivalentProperty have same "property extension"
# (P1 < P2) and (P2 < P1) => (P1 = P2)
#
[n=rule_equivalent_prop2, s=120]: \
(?P1 rdfs:subPropertyOf ?P2). \
(?P2 rdfs:subPropertyOf ?P1) \
-> \
(?P1 owl:equivalentProperty ?P2)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:inverseOf
#
# This applies to properties.
# ///////////////////////////////////////////////////////////////////
#
# owl:inverseOf is symetric and is applicable only to owl:ObjectProperty.
#
[n=rule_sym_inverse_prop1, s=120]: \
(?p1 owl:inverseOf ?p2) \
-> \
(?p2 owl:inverseOf ?p1). \
(?p1 rdf:type owl:ObjectProperty)
#
# owl:inverseOf have domain and range interchanged
#
[n=rule_domain_inverse_prop1, s=120]: \
(?p1 owl:inverseOf ?p2). \
(?p2 rdfs:domain ?c) \
-> \
(?p1 rdfs:range ?c)
[n=rule_range_inverse_prop1, s=120]: \
(?p1 owl:inverseOf ?p2). \
(?p2 rdfs:range ?c) \
-> \
(?p1 rdfs:domain ?c)
#
# P1 owl:inverseOf P2: P1(x, y) => P2(y, x)
#
[n=rule_pair_inverse_prop1, s=100]: \
(?p1 owl:inverseOf ?p2). \
(?s ?p1 ?o) \
-> \
(?o ?p2 ?s)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:FunctionalProperty
#
# This applies to properties.
# ///////////////////////////////////////////////////////////////////
#
# owl:FunctionalProperty can have only one value
#
[n=rule_functional_prop1, s=120]: \
(?p1 rdf:type owl:FunctionalProperty). \
(?s ?p1 ?o1). \
(?s ?p1 ?o2). \
[?o1 different_from ?o2] \
-> \
(?o1 owl:sameAs ?o2)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:InverseFunctionalProperty
#
# This applies to properties.
# ///////////////////////////////////////////////////////////////////
#
# owl:InverseFunctionalProperty is owl:ObjectProperty
#
[n=rule_inv_funct_prop1, s=120]: \
(?p1 rdf:type owl:InverseFunctionalProperty) \
-> \
(?p1 rdf:type owl:ObjectProperty) \
#
# owl:InverseFunctionalProperty can have only one subject
# P(x1, y) and P(x2, y) => (x1 = x2)
#
[n=rule_inv_funct_prop2, s=120]: \
(?p1 rdf:type owl:InverseFunctionalProperty). \
(?s1 ?p1 ?o). \
(?s2 ?p1 ?o). \
[?s1 different_from ?s2] \
-> \
(?s1 owl:sameAs ?s2)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:TransitiveProperty
#
# This applies to properties.
# ///////////////////////////////////////////////////////////////////
#
# owl:TransitiveProperty is owl:ObjectProperty
#
[n=rule_trans_prop1, s=120]: \
(?p1 rdf:type owl:TransitiveProperty) \
-> \
(?p1 rdf:type owl:ObjectProperty)
#
# owl:TransitiveProperty: P(x, y) ^ P(y, z) => P(x, z)
#
[n=rule_trans_prop2, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?s1 ?p1 ?s2). \
(?s2 ?p1 ?s3). \
[?s1 different_from ?s3] \
-> \
(?s1 ?p1 ?s3)
#
# owl:TransitiveProperty cannot have global cardinality constraints,
# nor it's superproperty, it's inverse, and the inverse of it's superproperty.
#
[n=rule_trans_prop3, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?p1 rdf:type owl:FunctionalProperty) \
-> \
(?p1 top:propertyError top:invalid_transitive_property)
[n=rule_trans_prop4, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?p1 rdf:type owl:InverseFunctionalProperty) \
-> \
(?p1 top:propertyError top:invalid_transitive_property)
[n=rule_trans_prop5, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 rdf:type owl:FunctionalProperty) \
-> \
(?p1 top:propertyError top:invalid_transitive_property)
[n=rule_trans_prop6, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 rdf:type owl:InverseFunctionalProperty) \
-> \
(?p1 top:propertyError top:invalid_transitive_property)
[n=rule_trans_prop7, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?p1 owl:inverseOf ?p2). \
(?p2 rdf:type owl:FunctionalProperty) \
-> \
(?p1 top:propertyError top:invalid_transitive_property)
[n=rule_trans_prop8, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?p1 owl:inverseOf ?p2). \
(?p2 rdf:type owl:InverseFunctionalProperty) \
-> \
(?p1 top:propertyError top:invalid_transitive_property)
[n=rule_trans_prop9, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 owl:inverseOf ?p3). \
(?p3 rdf:type owl:FunctionalProperty) \
-> \
(?p1 top:propertyError top:invalid_transitive_property)
[n=rule_trans_prop10, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?p1 rdfs:subPropertyOf ?p2). \
(?p2 owl:inverseOf ?p3). \
(?p3 rdf:type owl:InverseFunctionalProperty) \
-> \
(?p1 top:propertyError top:invalid_transitive_property)
#
# The superproperty of a transitive property is also a transitive property.
#
[n=rule_trans_prop11, s=120]: \
(?p1 rdf:type owl:TransitiveProperty). \
(?p1 rdfs:subPropertyOf ?p2) \
-> \
(?p2 rdf:type owl:TransitiveProperty)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:SymmetricProperty
#
# This applies to properties.
# ///////////////////////////////////////////////////////////////////
#
# owl:SymmetricProperty is owl:ObjectProperty
#
[n=rule_symetric_prop1, s=120]: \
(?p1 rdf:type owl:SymmetricProperty) \
-> \
(?p1 rdf:type owl:ObjectProperty)
#
# owl:SymmetricProperty: P(x, y) => P(y, x)
#
[n=rule_symetric_prop2, s=120]: \
(?p1 rdf:type owl:SymmetricProperty). \
(?x ?p1 ?y) \
-> \
(?y ?p1 ?x)
#
# The domain and range of a symmetric property are the same.
#
[n=rule_symetric_prop3, s=120]: \
(?p1 rdf:type owl:SymmetricProperty). \
(?p1 rdfs:domain ?c) \
-> \
(?p1 rdfs:range ?c)
#
# The domain and range of a symmetric property are the same.
#
[n=rule_symetric_prop4, s=120]: \
(?p1 rdf:type owl:SymmetricProperty). \
(?p1 rdfs:range ?c) \
-> \
(?p1 rdfs:domain ?c)
# ///////////////////////////////////////////////////////////////////
# LOGICAL CONSEQUENCES APPLICABLE TO PROPERTY RESTRICTION.
# ///////////////////////////////////////////////////////////////////
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:allValuesFrom
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# owl:allValuesFrom: Class where all individuals for which all values
# of the property under consideration are either members of the
# class extension of the class description or are data values within
# the specified data range:
# P all-values-from Y, for X: all y: P(x, y) and (y < Y) => (x < X)
#
# Assume all values will satisfy the condition, those who don't
# will be weed out.
#
[n=rule_all_value_from1, s=60]: \
(?c1 owl:allValuesFrom ?c2). \
(?c1 owl:onProperty ?p). \
(?o rdf:type ?c2). \
(?s ?p ?o). \
not(?s top:not_all_value_on ?p) \
-> \
(?s rdf:type ?c1)
#
# Weed out those who don't meet the criteria.
#
[n=rule_all_value_from2, s=70]: \
(?c1 owl:allValuesFrom ?c2). \
(?c1 owl:onProperty ?p). \
(?s ?p ?o). \
not(?o rdf:type ?c2) \
-> \
(?s top:not_all_value_on ?p)
#
# owl:allValuesFrom: Analogous to the universal (for-all) quantifier
# of Predicate logic:
# P all-values-from C: P(x, y) => (y < C)
#
[n=rule_all_value_from3, s=120]: \
(?c1 owl:allValuesFrom ?c2). \
(?c1 owl:onProperty ?p). \
(?s rdf:type ?c1). \
(?s ?p ?o) \
-> \
(?o rdf:type ?c2)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:someValuesFrom
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# owl:someValuesFrom: Describes a class of all individuals for which
# at least one value of the property concerned is an instance of the
# class description or a data value in the data range:
# P some-values-from Y, for X: exist y: P(x, y) and (y < Y) => (x < X)
#
[n=rule_some_value_from1, s=90]: \
(?c1 owl:someValuesFrom ?c2). \
(?c1 owl:onProperty ?p). \
(?o rdf:type ?c2). \
(?s ?p ?o) \
-> \
(?s rdf:type ?c1)
#
# owl:someValuesFrom: Analogous to the existential quantifier of Predicate logic;
# for each instance of the class that is being defined,
# there exists at least one value for P that fulfills the constraint:
# P some-values-from Y, for X: (x < X) => P(x, y) and (y < Y) [exist at least one y]
#
# Note: The enforcement here is reduced to determine whether
# the individual is consistent or not with the restriction.
#
[n=rule_some_value_from2, s=80]: \
(?c1 owl:someValuesFrom ?c2). \
(?c1 owl:onProperty ?p). \
(?s rdf:type ?c1). \
(?s ?p ?o). \
(?o rdf:type ?c2) \
-> \
(?s top:consistent_on ?p)
#
# Assume individuals are not consistent,
# those who are will be weed out.
#
[n=err_rule_some_value_from3, s=50]: \
(?c1 owl:someValuesFrom ?c2). \
(?c1 owl:onProperty ?p). \
(?s rdf:type ?c1). \
not(?s top:consistent_on ?p) \
-> \
(?s rdf:type owl:Nothing)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:hasValue
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# owl:hasValue: Describes a class of all individuals for which the
# property concerned has at least one value semantically equal to y:
# P has_value y, for X: P(x, y) => (x < X)
#
[n=rule_has_value1, s=100]: \
(?c1 owl:hasValue ?y). \
(?c1 owl:onProperty ?p). \
(?s ?p ?y) \
-> \
(?s rdf:type ?c1)
#
# All member of the described class must have at least one value
# sematically equal to y:
# P has_value y, for X: (x < X) => P(x, y)
#
[n=rule_has_value2, s=100]: \
(?c1 owl:hasValue ?y). \
(?c1 owl:onProperty ?p). \
(?s rdf:type ?c1) \
-> \
(?s ?p ?y)
#
# When the property concerned is a Transitive Property,
# then this class may be subclass to another one describing the
# set of individual with value obtained from transitivity:
# P has-value y, for X: as P(X, y)
# P is-transitive:
# P has-value y2, for X2: as P(X2, y2)
# P(X, y) and P(X2, y2) and P(y, y2) => (X < X2)
#
[n=rule_has_value3, s=100]: \
(?c1 owl:hasValue ?y1). \
(?c1 owl:onProperty ?P). \
(?P rdf:type owl:TransitiveProperty). \
(?c2 owl:hasValue ?y2). \
(?c2 owl:onProperty ?P). \
[?c1 different_from ?c2]. \
(?y1 ?P ?y2) \
-> \
(?c1 rdfs:subClassOf ?c2)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:maxCardinality
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# Describes a class of all individuals that have at most N semantically distinct values
# (individuals or data values) for the property concerned, where N is the value of the
# cardinality constraint.
#
#
# Identify the individuals: for X: (#P(x, y) .le. n) => (x < X)
#
[n=rule_max_cardinality1, s=5, o=f]: \
(?s top:cardinality_gate true). \
(?C owl:maxCardinality ?N). \
(?C owl:onProperty ?P). \
(?s ?P ?o). \
[?s test_max_cardinality ?C] \
-> \
(?s rdf:type ?C)
#
# Validate restriction: for X: (x < X) and not(#P(x, y) .le. n) => (x < 0)
#
[n=err_rule_max_cardinality2, s=5, o=f]: \
(?s top:cardinality_gate true). \
(?C owl:maxCardinality ?N). \
(?s rdf:type ?C). \
[not (?s test_max_cardinality ?C)] \
-> \
(?s rdf:type owl:Nothing)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:minCardinality
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# Describes a class of all individuals that have at least N semantically distinct values
# (individuals or data values) for the property concerned, where N is the value of the
# cardinality constraint.
#
#
# Identify the individuals: for X: (#P(x, y) .ge. n) => (x < X)
#
[n=rule_min_cardinality1, s=5, o=f]: \
(?s top:cardinality_gate true). \
(?C owl:minCardinality ?N). \
(?C owl:onProperty ?P). \
(?s ?P ?o). \
[?s test_min_cardinality ?C] \
-> \
(?s rdf:type ?C)
#
# Validate restriction: for X: (x < X) and not(#P(x, y) .ge. n) => (x < 0)
#
[n=err_rule_min_cardinality2, s=5, o=f]: \
(?s top:cardinality_gate true). \
(?C owl:minCardinality ?N). \
(?s rdf:type ?C). \
[not (?s test_min_cardinality ?C)] \
-> \
(?s rdf:type owl:Nothing)
# ///////////////////////////////////////////////////////////////////
# Apply logical consequences of
# owl:cardinality
#
# This applies to classes.
# ///////////////////////////////////////////////////////////////////
#
# Describes a class of all individuals that have exacly N semantically distinct values
# (individuals or data values) for the property concerned, where N is the value of the
# cardinality constraint.
#
#
# Identify the individuals: for X: (#P(x, y) .eq. n) => (x < X)
#
[n=rule_cardinality1, s=5, o=f]: \
(?s top:cardinality_gate true). \
(?C owl:cardinality ?N). \
(?C owl:onProperty ?P). \
(?s ?P ?o). \
[?s test_cardinality ?C] \
-> \
(?s rdf:type ?C)
#
# Validate restriction: for X: (x < X) and not(#P(x, y) .eq. n) => (x < 0)
#
[n=err_rule_cardinality2, s=5, o=f]: \
(?s top:cardinality_gate true). \
(?C owl:cardinality ?N). \
(?s rdf:type ?C). \
[not (?s test_cardinality ?C)] \
-> \
(?s rdf:type owl:Nothing)
#
# Gate to avoid rules to fires too early
#
[n=rule_gate_cardinality1, s=5, o=f]: \
(?C owl:maxCardinality ?N). \
(?s rdf:type ?C) \
-> \
(?s top:cardinality_gate true)
[n=rule_gate_cardinality2, s=5, o=f]: \
(?C owl:maxCardinality ?N). \
(?C owl:onProperty ?P). \
(?s ?P ?o) \
-> \
(?s top:cardinality_gate true)
[n=rule_gate_cardinality3, s=5, o=f]: \
(?C owl:minCardinality ?N). \
(?s rdf:type ?C) \
-> \
(?s top:cardinality_gate true)
[n=rule_gate_cardinality4, s=5, o=f]: \
(?C owl:minCardinality ?N). \
(?C owl:onProperty ?P). \
(?s ?P ?o) \
-> \
(?s top:cardinality_gate true)
[n=rule_gate_cardinality5, s=5, o=f]: \
(?C owl:cardinality ?N). \
(?s rdf:type ?C) \
-> \
(?s top:cardinality_gate true)
[n=rule_gate_cardinality6, s=5, o=f]: \
(?C owl:cardinality ?N). \
(?C owl:onProperty ?P). \
(?s ?P ?o) \
-> \
(?s top:cardinality_gate true)
#####################################################################
#####################################################################
#####################################################################
# ///////////////////////////////////////////////////////////////////
# query du jour. . .to avoid recompilation of unit test. . .
#
# ///////////////////////////////////////////////////////////////////
q_du_jour1: \
SELECT * FROM \
(?u top:propertyError ?x)
q_du_jour2: \
SELECT * FROM \
(?u rdfs:subClassOf owl:Nothing)
q_du_jour3: \
SELECT * FROM \
(?u ?v ?w). \
[((?v same_as rdfs:subClassOf) and \
((is_resource ?u) and (is_resource ?w)))]
q_du_jour4: \
SELECT * FROM \
(?u rdfs:subClassOf rdf:Property). \
(?u ?v ?w)
*knowledge-rules-end*
############################################################################
