#------------------------------------------------------------------ # OWL rule set v0.2 # This rule set is designed to implement owl(f)lite using the hybrid # rule system (mixture of forward and backward chaining). # # Warning: This version is under active development and the moment # and should NOT be regard as stable or usable. # # $Id: owl-fb-old.rules,v 1.2 2004-07-02 08:08:21 der Exp $ #------------------------------------------------------------------ #------------------------------------------------------------------ # RDFS Axioms #------------------------------------------------------------------ -> (rdf:type rdfs:range rdfs:Class). -> (rdfs:Resource rdf:type rdfs:Class). -> (rdfs:Literal rdf:type rdfs:Class). -> (rdf:Statement rdf:type rdfs:Class). -> (rdf:nil rdf:type rdf:List). -> (rdf:subject rdf:type rdf:Property). -> (rdf:object rdf:type rdf:Property). -> (rdf:predicate rdf:type rdf:Property). -> (rdf:first rdf:type rdf:Property). -> (rdf:rest rdf:type rdf:Property). -> (rdfs:subPropertyOf rdfs:domain rdf:Property). -> (rdfs:subClassOf rdfs:domain rdfs:Class). -> (rdfs:domain rdfs:domain rdf:Property). -> (rdfs:range rdfs:domain rdf:Property). -> (rdf:subject rdfs:domain rdf:Statement). -> (rdf:predicate rdfs:domain rdf:Statement). -> (rdf:object rdfs:domain rdf:Statement). -> (rdf:first rdfs:domain rdf:List). -> (rdf:rest rdfs:domain rdf:List). -> (rdfs:subPropertyOf rdfs:range rdf:Property). -> (rdfs:subClassOf rdfs:range rdfs:Class). -> (rdfs:domain rdfs:range rdfs:Class). -> (rdfs:range rdfs:range rdfs:Class). -> (rdf:type rdfs:range rdfs:Class). -> (rdfs:comment rdfs:range rdfs:Literal). -> (rdfs:label rdfs:range rdfs:Literal). -> (rdf:rest rdfs:range rdf:List). -> (rdf:Alt rdfs:subClassOf rdfs:Container). -> (rdf:Bag rdfs:subClassOf rdfs:Container). -> (rdf:Seq rdfs:subClassOf rdfs:Container). -> (rdfs:ContainerMembershipProperty rdfs:subClassOf rdf:Property). -> (rdfs:isDefinedBy rdfs:subPropertyOf rdfs:seeAlso). -> (rdf:XMLLiteral rdf:type rdfs:Datatype). -> (rdfs:Datatype rdfs:subClassOf rdfs:Class). #------------------------------------------------------------------ # RDFS Closure rules #------------------------------------------------------------------ # This one could be omitted since the results are not really very interesting! #[rdf1and4: (?x ?p ?y) -> (?p rdf:type rdf:Property), (?x rdf:type rdfs:Resource), (?y rdf:type rdfs:Resource)] [rdfs7b: (?a rdf:type rdfs:Class) -> (?a rdfs:subClassOf rdfs:Resource)] [rdfs2: (?p rdfs:domain ?c) -> [(?x rdf:type ?c) <- (?x ?p ?y)] ] [rdfs3: (?p rdfs:range ?c) -> [(?y rdf:type ?c) <- (?x ?p ?y), notFunctor(?y)] ] [rdfs5a: (?a rdfs:subPropertyOf ?b), (?b rdfs:subPropertyOf ?c) -> (?a rdfs:subPropertyOf ?c)] [rdfs5b: (?a rdf:type rdf:Property) -> (?a rdfs:subPropertyOf ?a)] [rdfs6: (?p rdfs:subPropertyOf ?q), notEqual(?p,?q) -> [ (?a ?q ?b) <- (?a ?p ?b)] ] [rdfs7: (?a rdf:type rdfs:Class) -> (?a rdfs:subClassOf ?a)] [rdfs8: (?a rdfs:subClassOf ?b), (?b rdfs:subClassOf ?c) -> (?a rdfs:subClassOf ?c)] [rdfs9: (?x rdfs:subClassOf ?y), notEqual(?x,?y) -> [ (?a rdf:type ?y) <- (?a rdf:type ?x)] ] [rdfs10: (?x rdf:type rdfs:ContainerMembershipProperty) -> (?x rdfs:subPropertyOf rdfs:member)] [rdfs2-partial: (?p rdfs:domain ?c) -> (?c rdf:type rdfs:Class)] [rdfs3-partial: (?p rdfs:range ?c) -> (?c rdf:type rdfs:Class)] #------------------------------------------------------------------ # RDFS iff extensions needed for OWL #------------------------------------------------------------------ [rdfs2a: (?x rdfs:domain ?y), (?y rdfs:subClassOf ?z) -> (?x rdfs:domain ?z)] [rdfs3a: (?x rdfs:range ?y), (?y rdfs:subClassOf ?z) -> (?x rdfs:range ?z)] [rdfs12a: (rdf:type rdfs:subPropertyOf ?z), (?z rdfs:domain ?y) -> (rdfs:Resource rdfs:subClassOf ?y)] [rdfs12a: (rdfs:subClassOf rdfs:subPropertyOf ?z), (?z rdfs:domain ?y) -> (rdfs:Class rdfs:subClassOf ?y)] [rdfs12a: (rdfs:subPropertyOf rdfs:subPropertyOf ?z), (?z rdfs:domain ?y) -> (rdf:Property rdfs:subClassOf ?y)] [rdfs12b: (rdfs:subClassOf rdfs:subPropertyOf ?z), (?z rdfs:range ?y) -> (rdfs:Class rdfs:subClassOf ?y)] [rdfs12b: (rdfs:subPropertyOf rdfs:subPropertyOf ?z), (?z rdfs:range ?y) -> (rdf:Property rdfs:subClassOf ?y)] #------------------------------------------------------------------ # OWL axioms #------------------------------------------------------------------ -> (rdf:first rdf:type owl:FunctionalProperty). -> (rdf:rest rdf:type owl:FunctionalProperty). -> (rdfs:domain owl:SymmetricProperty owl:ObjectProperty). -> (rdfs:domain owl:TransitiveProperty owl:ObjectProperty). -> (rdfs:domain owl:InverseFunctionalProperty owl:ObjectProperty). -> (rdfs:range owl:ObjectProperty owl:Thing). -> (rdfs:domain owl:ObjectProperty owl:Thing). -> (rdfs:domain owl:DatatypeProperty owl:Thing). -> (owl:Class rdfs:subClassOf rdfs:Class). -> (owl:Restriction rdfs:subClassOf owl:Class). # The distinction between rdfs and owl class with disappear. # Adding this in introduces rather a lot of duplicate reasoning paths # which slow things down for no purpose. #-> (rdfs:Class rdfs:subClassOf owl:Class). -> (owl:Thing rdf:type owl:Class). # These might need to be pre-expanded in the initial rule set -> (owl:equivalentProperty rdf:type owl:SymmetricProperty). -> (owl:equivalentProperty rdf:type owl:TransitiveProperty). -> (owl:equivalentClass rdf:type owl:SymmetricProperty). -> (owl:equivalentClass rdf:type owl:TransitiveProperty). -> (owl:sameIndividualAs rdf:type owl:SymmetricProperty). -> (owl:sameIndividualAs rdf:type owl:TransitiveProperty). -> (owl:sameIndividualAs owl:equivalentProperty owl:sameAs). -> (owl:differentFrom rdf:type owl:SymmetricProperty). -> (owl:intersectionOf rdfs:domain owl:Class). #------------------------------------------------------------------ # OWL Rules #------------------------------------------------------------------ [thing1: (?C rdf:type owl:Class) -> (?C rdfs:subClassOf owl:Thing)] #------------------------------------------------------------------ # Identify restriction assertions #------------------------------------------------------------------ [restriction1: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:someValuesFrom ?D) -> (?C owl:equivalentClass some(?P, ?D))] [restriction2: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:allValuesFrom ?D) -> (?C owl:equivalentClass all(?P, ?D))] [restriction3: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:minCardinality ?X) -> (?C owl:equivalentClass min(?P, ?X))] [restriction4: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:maxCardinality ?X) -> (?C owl:equivalentClass max(?P, ?X))] [restriction5: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:cardinality ?X) -> (?C owl:equivalentClass card(?P, ?X)), (?C rdfs:subClassOf min(?P, ?X)), (?C rdfs:subClassOf max(?P, ?X)) ] [restriction6: (?C rdfs:subClassOf min(?P, ?X)), (?C rdfs:subClassOf max(?P, ?X)) -> (?C rdfs:subClassOf card(?P, ?X))] # Needed for the case where ?R is a restriction literal # and so does not appear in the subject position [restrictionSubclass1: (?D owl:equivalentClass ?R), isFunctor(?R) -> [restrictionSubclass1b: (?X rdf:type ?D) <- (?X rdf:type ?R)] ] [restrictionSubclass2: (?D owl:equivalentClass ?R), isFunctor(?R) -> [restrictionSubclass2b: (?X rdf:type ?R) <- (?X rdf:type ?D)] ] # Temp trial - might replace above #[restrictionSubclass1: (?D owl:equivalentClass ?R), isFunctor(?R) , (?X rdf:type ?R) -> (?X rdf:type ?D)] #[restrictionSubclass2: (?D owl:equivalentClass ?R), isFunctor(?R) , (?X rdf:type ?D) -> (?X rdf:type ?R)] #------------------------------------------------------------------ # Interactions between cardinalities and some/all #------------------------------------------------------------------ [restrictionMS-A: (?C rdfs:subClassOf max(?P, 1)), (?C rdfs:subClassOf some(?P, ?D)) -> (?C rdfs:subClassOf all(?P, ?D)) ] [restrictionFS-A: (?P rdf:type owl:FunctionalProperty), (?C rdfs:subClassOf some(?P, ?C)) -> (?C rdfs:subClassOf all(?P, ?C)) ] [restrictionR-S: (?P rdfs:range ?C), notFunctor(?C) -> [restrictionRSb: (?X rdf:type some(?P, ?C)) <- (?X ?P ?A) ] ] [restrictionRMn-S: (?P rdfs:range ?D), (?C rdfs:subClassOf min(?P, 1)) -> (?C rdfs:subClassOf some(?P, ?D)) ] [restrictionRA-T: (?P rdfs:range ?C), (?D owl:equivalentClass all(?P, ?C)) -> (owl:Thing rdfs:subClassOf ?D) ] [restrictionFT-M: (?P rdf:type owl:FunctionalProperty) -> [restrictionFTMb: (?X rdf:type max(?P, 1)) <- (?X rdf:type owl:Thing)] ] # If leave this forward get #ranges * #classes deductions # The backward one is only safe if there are no interactions with other forward rules #[restrictionR-A: (?P rdfs:range ?C), (?D rdf:type owl:Class), notFunctor(?C) # -> (?D rdfs:subClassOf all(?P, ?C)) ] [restrictionR-A: (?D rdfs:subClassOf all(?P, ?C)) <- (?P rdfs:range ?C), (?D rdf:type owl:Class), notFunctor(?C) ] [restrictionA-R: (owl:Thing rdfs:subClassOf all(?P, ?C)) -> (?P rdfs:range ?C), (?P rdf:type owl:ObjectProperty) ] [restriction-S: (?X rdf:type some(?P, ?C)) <- bound(?P), bound(?X), (?X ?P ?V), (?V rdf:type ?C) ] [restrictionM-N: (?X rdf:type owl:Nothing) <- (?X rdf:type max(?P, 0)), (?X ?P ?A) ] [restrictionA-Ty: (?C rdfs:subClassOf all(?P, ?D)), notEqual(?P, rdf:type), notEqual(?C, ?D) -> [restrictionA-tyb: (?Y rdf:type ?D) <- (?X rdf:type ?C), (?X ?P ?Y) ] ] # A-Ty + -S implies this so it is redundant (?) #[restrictionA-S: (?C rdfs:subClassOf all(?P, ?D)), notEqual(?P, rdf:type) -> # [restrictionA-Sb: (?X rdf:type some(?P, ?D)) <- (?X rdf:type ?C), (?X ?P ?Y)] ] #[restrictionM-sI: (?B owl:sameIndividualAs ?C) <- (?A rdf:type max(?P, 1)), (?A ?P ?B), (?A ?P ?C) ] [restrictionM-sI: (?C rdfs:subClassOf max(?P, 1)) -> [restrictionM-sIb: (?B owl:sameIndividualAs ?C) <- (?A rdf:type ?C), (?A ?P ?B), (?A ?P ?C) ] ] [restrictionMM-N: (?X rdf:type owl:Nothing) <- (?X rdf:type min(?P, 1)), (?X rdf:type max(?P, 0)) ] #------------------------------------------------------------------ # Using some(P,C) restriction to infer P values for instances. # Since this is instance reasoning we should be doing this backwards. # But we have a problem with makeInstance that we can't create new triples # during b-rule processing because the deductions graph doesn't support # concurrent update. We will solve this eventually but for now we revert # to a forward rule solution. #------------------------------------------------------------------ #[restrictionS-in: (?C rdfs:subClassOf some(?P, ?D)), notEqual(?P, owl:sameIndividualAs), notEqual(?D, owl:Class), notEqual(?D, rdfs:Class) -> # [restrictionS-inb: (?x ?P ?t) <- (?x rdf:type some(?P, ?D)), makeInstance(?x, ?P, ?D, ?t), print('inb', ?x, ?P, ?t) ] # [restrictionS-inb2: (?t rdf:type ?D) <- (?x ?P ?t), noValue(?t, rdf:type), print('inb2', ?t, ?D, ?x) ] # ] [restrictionS-in: (?D rdfs:subClassOf some(?P,?C)) (?X rdf:type ?D), noValue(?X, ?P), notEqual(?P, owl:sameIndividualAs), notEqual(?C, owl:Class), notEqual(?C, rdfs:Class), notEqual(?P, rdfs:subClassOf), notEqual(?P, rdfs:subPropertyOf), notEqual(?P, owl:equivalentProperty), notEqual(?P, owl:equivalentClass), makeTemp(?T) -> (?X ?P ?T), (?T rdf:type ?C)] #------------------------------------------------------------------ # Create prototypical instances for each class and infer any subclass relations # This is better done as part of an explicit taxonomy building phase. # Note that prototype1 requires instance style reasoning so we need derivations # of type owl:Class to work forwards, hence the special type propagation rules. #------------------------------------------------------------------ [typeProp1: (?C rdf:type owl:Restriction) -> (?C rdf:type owl:Class) ] [typeProp2: (?C rdfs:subClassOf ?R), isFunctor(?R) -> (?C rdf:type owl:Class) ] [prototype1: (?c rdf:type owl:Class), noValue(?c, rb:prototype), makeTemp(?t) -> (?c rb:prototype ?t), (?t rdf:type ?c) ] #[prototype1: (?c rdf:type owl:Class), noValue(?c, rb:prototype), makeTemp(?t) # -> (?c rb:prototype ?t), (?t rdf:type ?c) # schedulePrototypeCheck(?p, ?c) ] #[prototype2a: (?c rb:prototype ?p), (?c rdfs:subClassOf ?d) (?d rdf:type owl:Restriction) # -> schedulePrototypeCheck(?p, ?c) ] #[prototype2b: (?c rb:prototype ?p), (?c rdf:type owl:Restriction) # -> schedulePrototypeCheck(?p, ?c) ] #[prototype2a: (?c rb:prototype ?p), (?c rdfs:subClassOf ?R) isFunctor(?R) # -> schedulePrototypeCheck(?p, ?c) ] # Back chain version [prototype2: (?c rb:prototype ?p) -> [prototype2b: (?c rdfs:subClassOf ?d) <- (?p rdf:type ?d)] ] [equivalentClass2b: (?P owl:equivalentClass ?Q) <- (?P rdfs:subClassOf ?Q), (?Q rdfs:subClassOf ?P) ] #------------------------------------------------------------------ # Disjointness #------------------------------------------------------------------ [distinct1: (?C owl:disjointWith ?D), (?X rdf:type ?C), (?Y rdf:type ?D) -> (?X owl:differentFrom ?Y) ] # Exploding the pairwise assertions is simply done procedurally here. # This is better handled by a dedicated equality reasoner any. [distinct2: (?w owl:distinctMembers ?L) -> assertDisjointPairs(?L) ] # Example version of validation rule, more TBD [validation1: (?X rdf:type owl:Nothing) <- (?X owl:differentFrom ?Y), (?X owl:sameIndividualAs ?Y)] #------------------------------------------------------------------ # Class equality #------------------------------------------------------------------ # equivalentClass [equivalentClass1: (?P owl:equivalentClass ?Q) -> (?P rdfs:subClassOf ?Q), (?Q rdfs:subClassOf ?P) ] [equivalentClass2: (?P rdfs:subClassOf ?Q), (?Q rdfs:subClassOf ?P) -> (?P owl:equivalentClass ?Q) ] [equivalentClass3: (?P owl:sameAs ?Q), (?P rdf:type rdfs:Class), (?Q rdf:type rdfs:Class) -> (?P owl:equivalentClass ?Q) ] #------------------------------------------------------------------ # Instance equality #------------------------------------------------------------------ # sameIndividualAs [sameIndividualAs1: (?P rdf:type owl:FunctionalProperty) -> [sameIndividualAs1b: (?B owl:sameIndividualAs ?C) <- unbound(?C), (?A ?P ?B), (?A ?P ?C) ] [sameIndividualAs1b: (?B owl:sameIndividualAs ?C) <- bound(?C), (?A ?P ?C), (?A ?P ?B) ] ] [sameIndividualAs2: (?P rdf:type owl:InverseFunctionalProperty) -> [sameIndividualAs2b: (?A owl:sameIndividualAs ?C) <- unbound(?C), (?A ?P ?B), (?C ?P ?B) ] [sameIndividualAs2b: (?A owl:sameIndividualAs ?C) <- bound(?C), (?C ?P ?B), (?A ?P ?B) ] ] # Raw version of above #[sameIndividualAs1: (?P rdf:type owl:FunctionalProperty) -> # [sameIndividualAs1b: (?B owl:sameIndividualAs ?C) <- (?A ?P ?B), (?A ?P ?C) ] ] # #[sameIndividualAs2: (?P rdf:type owl:InverseFunctionalProperty) -> # [sameIndividualAs2b: (?A owl:sameIndividualAs ?C) <- (?A ?P ?B), (?C ?P ?B) ] ] [sameIndividualAs3: (?X owl:sameAs ?Y), (?X rdf:type owl:Thing), (?Y rdf:type owl:Thing) -> (?X owl:sameIndividualAs ?Y) ] [sameIndividualAs4: (?Y ?P ?V) <- unbound(?V), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y), (?X ?P ?V) ] [sameIndividualAs4: (?Y ?P ?V) <- bound(?V), unbound(?P), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y), (?X ?P ?V) ] [sameIndividualAs4: (?Y ?P ?V) <- bound(?V), bound(?P), (?X ?P ?V) (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y) ] [sameIndividualAs5: (?V ?P ?Y) <- unbound(?V), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y), (?V ?P ?X) ] [sameIndividualAs5: (?V ?P ?Y) <- bound(?V), unbound(?P), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y), (?V ?P ?X) ] [sameIndividualAs5: (?V ?P ?Y) <- bound(?V), bound(?P), (?V ?P ?X), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y) ] [sameIndividualAs6: (?X rdf:type owl:Thing) <- (?X owl:sameIndividualAs ?Y) ] [sameIndividualAs6: (?Y rdf:type owl:Thing) <- (?X owl:sameIndividualAs ?Y) ] #------------------------------------------------------------------ # Property rules #------------------------------------------------------------------ # equivalentProperty [equivalentProperty1: (?P owl:equivalentProperty ?Q) -> (?P rdfs:subPropertyOf ?Q), (?Q rdfs:subPropertyOf ?P) ] [equivalentProperty2: (?P rdfs:subPropertyOf ?Q), (?Q rdfs:subPropertyOf ?P) -> (?P owl:equivalentProperty ?Q) ] [equivalentProperty3: (?P owl:sameAs ?Q), (?P rdf:type rdf:Property), (?Q rdf:type rdf:Property) -> (?P owl:equivalentProperty ?Q) ] # symmetric [symmetricProperty1: (?P rdf:type owl:SymmetricProperty) -> [symmetricProperty1b: (?X ?P ?Y) <- (?Y ?P ?X)] ] # inverseOf [inverseOf1: (?P owl:inverseOf ?Q) -> (?Q owl:inverseOf ?P) ] [inverseOf2: (?P owl:inverseOf ?Q) -> [inversOf2b: (?X ?P ?Y) <- (?Y ?Q ?X)] ] [inverseOf3: (?P owl:inverseOf ?Q), (?P rdf:type owl:FunctionalProperty) -> (?Q rdf:type owl:InverseFunctionalProperty) ] [inverseOf4: (?P owl:inverseOf ?Q), (?P rdf:type owl:InverseFunctionalProperty) -> (?Q rdf:type owl:FunctionalProperty) ] # Transitive [transitiveProperty1: (?P rdf:type owl:TransitiveProperty) -> [transitiveProperty1b: (?A ?P ?C) <- (?A ?P ?B), (?B ?P ?C)] ] #------------------------------------------------------------------ # if-only parts of additional constructs #------------------------------------------------------------------ # hasValue [hasValue1: (?c rdf:type owl:Restriction), (?c owl:onProperty ?p), (?c owl:hasValue ?v) -> [hasValue1b: (?x ?p ?v) <- (?x rdf:type ?c) ] ] #------------------------------------------------------------------ # Unused rules - attempted tuning but builtin clause reordering does well enough #------------------------------------------------------------------ #[transitiveProperty1: (?P rdf:type owl:TransitiveProperty) -> # [transitiveProperty1b: (?A ?P ?C) <- unbound(?C), (?A ?P ?B), (?B ?P ?C)] # [transitiveProperty1b: (?A ?P ?C) <- bound(?C), (?B ?P ?C), (?A ?P ?B)] # ]