http://git-wip-us.apache.org/repos/asf/jena/blob/4b5cd267/jena-core/src/main/resources/etc/owl-fb-mini.rules
----------------------------------------------------------------------
diff --cc jena-core/src/main/resources/etc/owl-fb-mini.rules
index 12d43b9,12d43b9..fb6792e
--- a/jena-core/src/main/resources/etc/owl-fb-mini.rules
+++ b/jena-core/src/main/resources/etc/owl-fb-mini.rules
@@@ -1,748 -1,748 +1,748 @@@
--# Licensed to the Apache Software Foundation (ASF) under one
--# or more contributor license agreements. See the NOTICE file
--# distributed with this work for additional information
--# regarding copyright ownership. The ASF licenses this file
--# to you under the Apache License, Version 2.0 (the
--# "License"); you may not use this file except in compliance
--# with the License. You may obtain a copy of the License at
--#
--# http://www.apache.org/licenses/LICENSE-2.0
--#
--# Unless required by applicable law or agreed to in writing, software
--# distributed under the License is distributed on an "AS IS" BASIS,
--# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--# See the License for the specific language governing permissions and
--# limitations under the License.
--
--#------------------------------------------------------------------
--# OWL mini rule set v 0.1
--#
--# This is identical to the normal OWL rules except for:
--# - omit XSD range inheritance
--# - omit bNode introductin for someValuesFrom and minCardality
--#
--# $Id: owl-fb.rules,v 1.47 2004/03/09 18:36:30 der Exp $
--#------------------------------------------------------------------
--
--#------------------------------------------------------------------
--# Tabling directives
--#------------------------------------------------------------------
--
---> tableAll().
--
--#-> table(rdf:type).
--#-> table(rdfs:subClassOf).
--#-> table(rdfs:range).
--#-> table(rdfs:domain).
--#-> table(owl:equivalentClass).
--
--#------------------------------------------------------------------
--# 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)]
--[rdf4: (?x ?p ?y) -> (?p rdf:type rdf:Property)]
--
--[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)]
--[rdfs5b: (?a rdfs:subPropertyOf ?a) <- (?a rdf:type rdf:Property)]
--[rdfs6: (?p rdfs:subPropertyOf ?q), notEqual(?p,?q) -> [ (?a ?q ?b) <- (?a
?p ?b)] ]
--[rdfs7: (?a rdf:type rdfs:Class) -> (?a rdfs:subClassOf ?a)]
--# omit rdfs8, derivable from rdfs9 and prototype2
--[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 ?z) <- bound(?x), (?x rdfs:domain ?y), (?y
rdfs:subClassOf ?z) ]
--[rdfs2a: (?x rdfs:domain ?z) <- unbound(?x), (?y rdfs:subClassOf ?z), (?x
rdfs:domain ?y) ]
--[rdfs3a: (?x rdfs:range ?z) <- bound(?x), (?x rdfs:range ?y), (?y
rdfs:subClassOf ?z) ]
--[rdfs3a: (?x rdfs:range ?z) <- unbound(?x), (?y rdfs:subClassOf ?z), (?x
rdfs:range ?y) ]
--
--[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)]
--
--[rdfsder1: (?p rdfs:range ?z) <- (?p rdfs:subPropertyOf ?q), notEqual(?p,
?q), (?q rdfs:range ?z)]
--[rdfsder2: (?p rdfs:domain ?z) <- (?p rdfs:subPropertyOf ?q), notEqual(?p,
?q), (?q rdfs:domain ?z)]
--
--#------------------------------------------------------------------
--# OWL axioms
--#------------------------------------------------------------------
--
---> (owl:FunctionalProperty rdfs:subClassOf rdf:Property).
---> (owl:ObjectProperty rdfs:subClassOf rdf:Property).
---> (owl:DatatypeProperty rdfs:subClassOf rdf:Property).
---> (owl:InverseFunctionalProperty rdfs:subClassOf owl:ObjectProperty).
---> (owl:TransitiveProperty rdfs:subClassOf owl:ObjectProperty).
---> (owl:SymmetricProperty rdfs:subClassOf owl:ObjectProperty).
--
---> (rdf:first rdf:type owl:FunctionalProperty).
---> (rdf:rest rdf:type owl:FunctionalProperty).
--
---> (owl:oneOf rdfs:domain owl:Class).
--
---> (owl:Class rdfs:subClassOf rdfs:Class).
---> (owl:Restriction rdfs:subClassOf owl:Class).
--
---> (owl:Thing rdf:type owl:Class).
---> (owl:Nothing rdf:type owl:Class).
--
---> (owl:equivalentClass rdfs:domain owl:Class).
---> (owl:equivalentClass rdfs:range owl:Class).
--
---> (owl:disjointWith rdfs:domain owl:Class).
---> (owl:disjointWith rdfs:range owl:Class).
--
---> (owl:sameAs rdf:type owl:SymmetricProperty).
--#-> (owl:sameIndividualAs owl:equivalentProperty owl:sameAs).
--
--# These are true but mess up the Ont API's notion of declared properties
--#-> (owl:sameAs rdfs:domain owl:Thing).
--#-> (owl:sameAs rdfs:range owl:Thing).
--#-> (owl:differentFrom rdfs:domain owl:Thing).
--#-> (owl:differentFrom rdfs:range owl:Thing).
--
---> (owl:onProperty rdfs:domain owl:Restriction).
---> (owl:onProperty rdfs:range owl:Property).
--
---> (owl:OntologyProperty rdfs:subClassOf rdf:Property).
---> (owl:imports rdf:type owl:OntologyProperty).
---> (owl:imports rdfs:domain owl:Ontology).
---> (owl:imports rdfs:range owl:Ontology).
--
---> (owl:priorVersion rdfs:domain owl:Ontology).
---> (owl:priorVersion rdfs:range owl:Ontology).
--
---> (owl:backwardCompatibleWith rdfs:domain owl:Ontology).
---> (owl:backwardCompatibleWith rdfs:range owl:Ontology).
--
---> (owl:incompatibleWith rdfs:domain owl:Ontology).
---> (owl:incompatibleWith rdfs:range owl:Ontology).
--
---> (owl:versionInfo rdf:type owl:AnnotationProperty).
--
--# These properties are derivable from the definitions
--#-> (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:differentFrom rdf:type owl:SymmetricProperty).
---> (owl:disjointWith rdf:type owl:SymmetricProperty).
--
---> (owl:intersectionOf rdfs:domain owl:Class).
--
--#------------------------------------------------------------------
--# OWL Rules
--#------------------------------------------------------------------
--
--[thing1: (?C rdf:type owl:Class) -> (?C rdfs:subClassOf owl:Thing)]
--
--#------------------------------------------------------------------
--# One direction of unionOf
--#------------------------------------------------------------------
--
--[unionOf1: (?C owl:unionOf ?L) -> listMapAsSubject(?L, rdfs:subClassOf ?C) ]
--
--# Note could also add relation between two unionOf's if we add a listSubsumes
primitive
--
--#------------------------------------------------------------------
--# Prototype rules to convert instance reasoning to class subsumption checking
--#------------------------------------------------------------------
--
--[earlyTypeProp1: (?C rdf:type owl:Restriction) -> (?C rdf:type owl:Class) ]
--
--[earlyTypeProp2: (?C owl:intersectionOf ?X) -> (?C rdf:type owl:Class) ]
--
--[earlyTypeProp3: (?C rdf:type owl:Class) -> (?C rdf:type rdfs:Class) ]
--
--[prototype1: (?c rdf:type owl:Class), noValue(?c, rb:prototype), notEqual(?c,
owl:Nothing), makeTemp(?t), hide(?t)
-- -> (?c rb:prototype ?t), (?t rdf:type ?c) ]
--
--[prototype2: (?c rb:prototype ?p) ->
-- [prototype2b: (?c rdfs:subClassOf ?d) <- (?p rdf:type ?d)] ]
--
--#------------------------------------------------------------------
--# Identify restriction assertions
--#------------------------------------------------------------------
--
--[restriction1: (?C owl:onProperty ?P), (?C owl:someValuesFrom ?D)
-- -> (?C owl:equivalentClass some(?P, ?D))]
--
--[restriction2: (?C owl:onProperty ?P), (?C owl:allValuesFrom ?D)
-- -> (?C owl:equivalentClass all(?P, ?D))]
--
--[restriction3: (?C owl:onProperty ?P), (?C owl:minCardinality ?X)
-- -> (?C owl:equivalentClass min(?P, ?X))]
--
--[restriction4: (?C owl:onProperty ?P), (?C owl:maxCardinality ?X)
-- -> (?C owl:equivalentClass max(?P, ?X)) ]
--
--[restriction5: (?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))]
--
--# Could limit the work done here by inserting an isFunctor guard?
--[restrictionPropagate1: (?C owl:equivalentClass ?R), (?D rdfs:subClassOf ?C)
-- -> (?D rdfs:subClassOf ?R) ]
--[restrictionPropagate2: (?C owl:equivalentClass ?R), (?D owl:equivalentClass
?C)
-- -> (?D owl:equivalentClass ?R) ]
--
--# 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)] ]
--
--# This is redundant because equivalentClass is symmetric anyway
--#[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)]
--
--#------------------------------------------------------------------
--# min cardinality
--#------------------------------------------------------------------
--
--[minRec: (?C owl:equivalentClass min(?P, 1)), notEqual(?P, rdf:type) ->
-- [min2b: (?X rdf:type ?C) <- (?X ?P ?Y)] ]
--
--[restriction-inter-MnS: (?P rdfs:range ?D), (?C rdfs:subClassOf min(?P, 1))
-- -> (?C rdfs:subClassOf some(?P, ?D)) ]
--
--#------------------------------------------------------------------
--# max cardinality 1
--#------------------------------------------------------------------
--
--# Rule move to sameInstance block below to ease experimentation
--#[max1: (?C rdfs:subClassOf max(?P, 1)) ->
--# [max1b: (?Y1 owl:sameAs ?Y2) <- bound(?Y1), (?X ?P ?Y1), (?X rdf:type
?C), (?X ?P ?Y2), notEqual(?Y1, ?Y2)]
--# [max1b: (?Y1 owl:sameAs ?Y2) <- unbound(?Y1), (?X ?P ?Y2), (?X rdf:type
?C), (?X ?P ?Y1), notEqual(?Y1, ?Y2)]
--# ]
--
--[maxRec: (?C owl:equivalentClass max(?P, 1)), (?P rdf:type
owl:FunctionalProperty) ->
-- [ (?X rdf:type ?C) <- (?X rdf:type owl:Thing)] ]
--
--#------------------------------------------------------------------
--# max cardinality 0
--#------------------------------------------------------------------
--
--# For completeness this requires iff version of rdfs:domain working forwards
which it does not just now
--[maxRec2: (?C owl:equivalentClass max(?P, 0)), (?P rdfs:domain ?D), (?E
owl:disjointWith ?D)
-- -> (?E rdfs:subClassOf ?C)]
--
--[cardRec1: (?C owl:equivalentClass card(?P, 0)), (?P rdfs:domain ?D), (?E
owl:disjointWith ?D)
-- -> (?E rdfs:subClassOf ?C)]
--
--[cardRec3: (?C owl:equivalentClass card(?P, 0)) ->
-- [cardRec2b: (?X rdf:type ?C) <- (?X rdf:type max(?P, 0))] ]
--
--#------------------------------------------------------------------
--# cardinality 1
--#------------------------------------------------------------------
--
--[restriction-inter-CFP: (?C owl:equivalentClass card(?P, 1)), (?P rdf:type
owl:FunctionalProperty) ->
-- (?C owl:equivalentClass min(?P, 1)) ]
--
--[cardRec2: (?C owl:equivalentClass card(?P, 1)) ->
-- [cardRec2b: (?X rdf:type ?C) <- (?X rdf:type min(?P, 1)), (?X rdf:type
max(?P, 1)) ] ]
--
--#------------------------------------------------------------------
--# someValuesFrom
--#------------------------------------------------------------------
--
--#[someRec: (?C owl:equivalentClass some(?P, ?D)), (?P rdfs:range ?D) ->
--# [someRecb: (?X rdf:type ?C) <- (?X ?P ?A) ] ]
--
--[someRec2: (?C owl:equivalentClass some(?P, ?D)) ->
-- [someRec2b: (?X rdf:type ?C) <- (?X ?P ?A) (?A rdf:type ?D) ] ]
--
--[someRec2b: (?C owl:equivalentClass some(?P, ?D)), (?D rdf:type
rdfs:Datatype)->
-- [someRec2b: (?X rdf:type ?C) <- (?X ?P ?A), isDType(?A, ?D) ] ]
--
--#------------------------------------------------------------------
--# allValuesFrom
--#------------------------------------------------------------------
--
--[all1: (?C rdfs:subClassOf all(?P, ?D)), notEqual(?P, rdf:type), notEqual(?C,
?D) ->
-- [all1b: (?Y rdf:type ?D) <- (?X ?P ?Y), (?X rdf:type ?C) ] ]
--
--[allRec1: (?C rdfs:subClassOf max(?P, 1)), (?C rdfs:subClassOf some(?P, ?D))
-- -> (?C rdfs:subClassOf all(?P, ?D)) ]
--
--[allRec2: (?P rdf:type owl:FunctionalProperty), (?C rdfs:subClassOf some(?P,
?C))
-- -> (?C rdfs:subClassOf all(?P, ?C)) ]
--
--[allRec3: (?C owl:equivalentClass all(?P, ?D)), (?P rdfs:range ?D) ->
-- [ (?X rdf:type ?C) <- (?X rdf:type owl:Thing)] ]
--
--[allRec4: (?P rdf:type owl:FunctionalProperty), (?C owl:equivalentClass
all(?P, ?D))
-- -> [ (?X rdf:type ?C) <- (?X ?P ?Y) (?Y rdf:type ?D)
] ]
--
--[allRec5: (?C rdfs:subClassOf max(?P, 1)) (?C owl:equivalentClass all(?P, ?D))
-- -> [ (?X rdf:type ?C) <- (?X ?P ?Y) (?Y rdf:type ?D)
] ]
--
--[restriction-inter-RA-T: (?P rdfs:range ?C), (?D owl:equivalentClass all(?P,
?C))
-- -> (owl:Thing rdfs:subClassOf ?D) ]
--
--[restriction-inter-AT-R: (owl:Thing rdfs:subClassOf all(?P, ?C))
-- -> (?P rdfs:range ?C), (?P rdf:type owl:ObjectProperty) ]
--
--# This version looks strange but we are experimenting with droping the direct
--# subclass transitive closure and inferring from prototypes, but that is being
--# done backwards for forwards subclass relationships are handled as special
cases
--#[restriction-inter-AT-R: (owl:Thing rdfs:subClassOf ?D) (?D
owl:equivalentClass all(?P, ?C))
--# -> (?P rdfs:range ?C), (?P
rdf:type owl:ObjectProperty) ]
--
--#------------------------------------------------------------------
--# Nothing
--#------------------------------------------------------------------
--
--[nothing1: (?C rdfs:subClassOf min(?P, ?n)) (?C rdfs:subClassOf max(?P, ?x))
-- lessThan(?x, ?n) -> (?C owl:equivalentClass owl:Nothing) ]
--
--[nothing2: (?C rdfs:subClassOf ?D) (?C rdfs:subClassOf ?E) (?D
owl:disjointWith ?E)
-- -> (?C owl:equivalentClass owl:Nothing) ]
--
--[nothing3: (?C rdfs:subClassOf owl:Nothing) -> (?C owl:equivalentClass
owl:Nothing) ]
--
--[nothing4: (?C owl:oneOf rdf:nil) -> (?C owl:equivalentClass owl:Nothing) ]
--
--#------------------------------------------------------------------
--# Disjointness
--#------------------------------------------------------------------
--
--#[distinct1: (?C owl:disjointWith ?D), (?X rdf:type ?C), (?Y rdf:type ?D)
--# -> (?X owl:differentFrom ?Y) ]
--
--[distinct1: (?X owl:differentFrom ?Y) <-
-- (?C owl:disjointWith ?D), (?X rdf:type ?C), (?Y rdf:type ?D) ]
--
--# 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) ]
--
--#------------------------------------------------------------------
--# Class equality
--#------------------------------------------------------------------
--
--# equivalentClass
--[equivalentClass1: (?P owl:equivalentClass ?Q)
-- -> (?P rdfs:subClassOf ?Q), (?Q rdfs:subClassOf ?P) ]
--
--[equivalentClass2: (?P owl:equivalentClass ?Q) <- (?P rdfs:subClassOf ?Q),
(?Q rdfs:subClassOf ?P) ]
--
--[equivalentClass3: (?P owl:sameAs ?Q), (?P rdf:type rdfs:Class), (?Q rdf:type
rdfs:Class)
-- -> (?P owl:equivalentClass ?Q) ]
--
--#------------------------------------------------------------------
--# Instance equality
--#------------------------------------------------------------------
--
--# sameAs
--
--#[sameAs1: (?P rdf:type owl:FunctionalProperty) ->
--# [sameAs1b: (?B owl:sameAs ?C) <- unbound(?C), (?A ?P ?B), (?A ?P ?C) ]
--# [sameAs1b: (?B owl:sameAs ?C) <- bound(?C), (?A ?P ?C), (?A ?P ?B) ]
--# ]
--#
--#[sameAs2: (?P rdf:type owl:InverseFunctionalProperty) ->
--# [sameAs2b: (?A owl:sameAs ?C) <- unbound(?C), (?A ?P ?B), (?C ?P ?B) ]
--# [sameAs2b: (?A owl:sameAs ?C) <- bound(?C), (?C ?P ?B), (?A ?P ?B) ]
--# ]
--#
--##[sameAs3: (?X owl:sameAs ?Y), (?X rdf:type owl:Thing), (?Y rdf:type
owl:Thing)
--## -> (?X owl:sameAs ?Y) ]
--#
--#[sameAs4a: (?Y ?P ?V) <- unbound(?V), (?X owl:sameAs ?Y), notEqual(?X,?Y),
(?X ?P ?V) ]
--#[sameAs4c: (?Y ?P ?V) <- bound(?V), (?X ?P ?V), notEqual(?X,?Y), (?X
owl:sameAs ?Y) ]
--#[sameAs5a: (?V ?P ?Y) <- unbound(?V), (?X owl:sameAs ?Y), notEqual(?X,?Y),
(?V ?P ?X) ]
--#[sameAs5c: (?V ?P ?Y) <- bound(?V), (?V ?P ?X), notEqual(?X,?Y), (?X
owl:sameAs ?Y) ]
--#
--#[sameAs6: (?X rdf:type owl:Thing) <- (?X owl:sameAs ?Y) ]
--##[sameAs6: (?Y rdf:type owl:Thing) <- (?X owl:sameAs ?Y) ]
--
--#------------------------------------------------------------------
--# Experimental forward version of instance equality
--#------------------------------------------------------------------
--
--# sameAs recognition rules - forward version
--
--[fp1: (?P rdf:type owl:FunctionalProperty), (?A ?P ?B), notLiteral(?B), (?A
?P ?C), notLiteral(?C)
-- notEqual(?B, ?C) -> (?B owl:sameAs ?C) ]
--
--[ifp1: (?P rdf:type owl:InverseFunctionalProperty), (?A ?P ?B), (?C ?P ?B)
-- notEqual(?A, ?C) -> (?A owl:sameAs ?C) ]
--
--[fp1: (?P rdf:type owl:FunctionalProperty), (?A ?P ?B), notLiteral(?B), (?A
?Q ?C), notLiteral(?C),
-- notEqual(?B, ?C), (?Q rdfs:subPropertyOf ?P) -> (?B owl:sameAs ?C) ]
--
--[ifp1: (?P rdf:type owl:InverseFunctionalProperty), (?A ?P ?B), (?C ?Q ?B)
-- notEqual(?A, ?C), (?Q rdfs:subPropertyOf ?P) -> (?A owl:sameAs ?C)
]
--
--[fpEarlyProp: (?P rdf:type owl:FunctionalProperty) (?Q rdfs:subPropertyOf ?P)
->
-- (?Q rdf:type owl:FunctionalProperty) ]
--
--[ifpEarlyProp: (?P rdf:type owl:InverseFunctionalProperty) (?Q
rdfs:subPropertyOf ?P) ->
-- (?Q rdf:type owl:InverseFunctionalProperty) ]
--
--# This rule is not sufficient if the type inference is being done backwards
--[max1: (?C rdfs:subClassOf max(?P, 1)), (?X ?P ?Y1), notLiteral(?Y1), (?X
rdf:type ?C), (?X ?P ?Y2), notLiteral(?Y2),
-- notEqual(?Y1, ?Y2) -> (?Y1 owl:sameAs ?Y2) ]
--
--# Subclass inheritance not normally availabe forward which causes problems
for max1,
--# patch this but just for restrictions to limit costs
--[subClassTemp: (?C rdfs:subClassOf ?R), isFunctor(?R), (?B rdfs:subClassOf
?C) -> (?B rdfs:subClassOf ?R) ]
--
--# sameAs propagation rules - forward version
--
--[sameAs1: (?A owl:sameAs ?B) -> (?B owl:sameAs ?A) ]
--
--[sameAs2: (?A owl:sameAs ?B) (?B owl:sameAs ?C) -> (?A owl:sameAs ?C) ]
--
--[sameAs6: (?X rdf:type owl:Thing) <- (?X owl:sameAs ?Y) ]
--
--# Was
--# [sameAs7: (?X owl:sameAs ?X) <- bound(?X) (?X rdf:type owl:Thing) ]
--# which is not complete and breaks the find() contract.
--# Investigate why I though this was a useful thing to do in the first place!
--[sameAs7: (?X owl:sameAs ?X) <- (?X rdf:type owl:Thing) ]
--
--# Equality processing rules
--
--[equality1: (?X owl:sameAs ?Y), notEqual(?X,?Y) ->
-- [(?X ?P ?V) <- (?Y ?P ?V)]
-- [(?V ?P ?X) <- (?V ?P ?Y)] ]
--
--[equality2: (?X owl:sameAs ?Y), (?X rdf:type owl:Class) -> (?X
owl:equivalentClass ?Y) ]
--
--[equality3: (?X owl:sameAs ?Y), (?X rdf:type rdf:Property) -> (?X
owl:equivalentProperty ?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 rdfs:Property), (?Q
rdf:type rdfs:Property)
-- -> (?P owl:equivalentProperty ?Q) ]
--
--# SymmetricProperty
--
--[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) -> [inverseOf2b: (?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) ]
--
--[inverseof5: (?P owl:inverseOf ?Q) (?P rdfs:range ?C) -> (?Q rdfs:domain ?C)]
--[inverseof6: (?P owl:inverseOf ?Q) (?P rdfs:domain ?C) -> (?Q rdfs:range ?C)]
--
--# TransitiveProperty
--
--[transitiveProperty1: (?P rdf:type owl:TransitiveProperty) ->
--# [transitiveProperty1b: (?A ?P ?C) <- (?A ?P ?B), (?B
?P ?C)] ]
-- [transitiveProperty1b: (?A ?P ?C) <- bound (?C), (?B ?P ?C), (?A ?P
?B)]
-- [transitiveProperty1b: (?A ?P ?C) <- unbound (?C), (?A ?P ?B) (?B ?P
?C)]
-- ]
--
--# Object properties
--
--[objectProperty: (?P rdf:type owl:ObjectProperty) ->
-- (?P rdfs:domain owl:Thing) (?P rdfs:range owl:Thing) ]
--
--#------------------------------------------------------------------
--# Restricted support for hasValue, even though that is beyond OWL/lite
--#------------------------------------------------------------------
--
--# hasValue
--[hasValueRec: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C
owl:hasValue ?V)
-- -> (?C owl:equivalentClass hasValue(?P, ?V)) ]
--
--[hasValueIF: (?C owl:equivalentClass hasValue(?P, ?V)) ->
-- [ (?x ?P ?V) <- (?x rdf:type ?C) ]
-- [ (?x rdf:type ?C) <- (?x ?P ?V) ]
-- ]
--
--[hasValueProp: (?P rdf:type owl:FunctionalProperty) (?Q rdf:type
owl:FunctionalProperty)
-- (?P rdfs:domain ?D) (?Q rdfs:domain ?D)
-- (?D owl:equivalentClass hasValue(?P, ?V))
-- (?D owl:equivalentClass hasValue(?Q, ?V))
-- -> (?P owl:equivalentProperty ?Q)]
--
--
--#------------------------------------------------------------------
--# Restricted support for oneOf, even though that is beyond OWL/lite
--#------------------------------------------------------------------
--
--[oneOfFP: (?P rdfs:range ?C) (?C owl:oneOf ?l) (?l rdf:first ?x) (?l rdf:rest
rdf:nil)
-- -> (?P rdf:type owl:FunctionalProperty) ]
--
--[oneOfIFP: (?P rdfs:domain ?C) (?C owl:oneOf ?l) (?l rdf:first ?x) (?l
rdf:rest rdf:nil)
-- -> (?P rdf:type owl:InverseFunctionalProperty) ]
--
--[oneOf1: (?C owl:oneOf ?l) -> listMapAsSubject(?l, rdf:type, ?C) ]
--
--[oneOf2: (?C owl:oneOf ?l1) (?D owl:oneOf ?l2) notEqual(?l1, ?l2)
listEqual(?l1, ?l2) -> (?C owl:equivalentClass ?D) ]
--
--[oneOf3: (?C owl:oneOf ?l) (?l rdf:first ?x) (?l rdf:rest rdf:nil) ->
-- [ (?Y ?P ?x) <- (?Y ?P ?I) (?I rdf:type ?C) ] ]
--
--#------------------------------------------------------------------
--# Declaration of main XSD datatypes
--#------------------------------------------------------------------
--
---> (xsd:float rdf:type rdfs:Datatype).
---> (xsd:double rdf:type rdfs:Datatype).
---> (xsd:int rdf:type rdfs:Datatype).
---> (xsd:long rdf:type rdfs:Datatype).
---> (xsd:short rdf:type rdfs:Datatype).
---> (xsd:byte rdf:type rdfs:Datatype).
---> (xsd:unsignedByte rdf:type rdfs:Datatype).
---> (xsd:unsignedShort rdf:type rdfs:Datatype).
---> (xsd:unsignedInt rdf:type rdfs:Datatype).
---> (xsd:unsignedLong rdf:type rdfs:Datatype).
---> (xsd:decimal rdf:type rdfs:Datatype).
---> (xsd:integer rdf:type rdfs:Datatype).
---> (xsd:nonPositiveInteger rdf:type rdfs:Datatype).
---> (xsd:nonNegativeInteger rdf:type rdfs:Datatype).
---> (xsd:positiveInteger rdf:type rdfs:Datatype).
---> (xsd:negativeInteger rdf:type rdfs:Datatype).
---> (xsd:boolean rdf:type rdfs:Datatype).
---> (xsd:string rdf:type rdfs:Datatype).
---> (xsd:anyURI rdf:type rdfs:Datatype).
---> (xsd:hexBinary rdf:type rdfs:Datatype).
---> (xsd:base64Binary rdf:type rdfs:Datatype).
---> (xsd:date rdf:type rdfs:Datatype).
---> (xsd:time rdf:type rdfs:Datatype).
---> (xsd:dateTime rdf:type rdfs:Datatype).
---> (xsd:duration rdf:type rdfs:Datatype).
---> (xsd:gDay rdf:type rdfs:Datatype).
---> (xsd:gMonth rdf:type rdfs:Datatype).
---> (xsd:gYear rdf:type rdfs:Datatype).
---> (xsd:gYearMonth rdf:type rdfs:Datatype).
---> (xsd:gMonthDay rdf:type rdfs:Datatype).
--
---> (xsd:integer rdfs:subClassOf xsd:decimal).
--
---> hide(rb:xsdBase).
---> hide(rb:xsdRange).
---> hide(rb:prototype).
--
---> (xsd:byte rb:xsdBase xsd:decimal).
---> (xsd:short rb:xsdBase xsd:decimal).
---> (xsd:int rb:xsdBase xsd:decimal).
---> (xsd:long rb:xsdBase xsd:decimal).
---> (xsd:unsignedByte rb:xsdBase xsd:decimal).
---> (xsd:unsignedShort rb:xsdBase xsd:decimal).
---> (xsd:unsignedInt rb:xsdBase xsd:decimal).
---> (xsd:unsignedLong rb:xsdBase xsd:decimal).
---> (xsd:integer rb:xsdBase xsd:decimal).
---> (xsd:nonNegativeInteger rb:xsdBase xsd:decimal).
---> (xsd:nonPositiveInteger rb:xsdBase xsd:decimal).
---> (xsd:byte rb:xsdBase xsd:decimal).
---> (xsd:float rb:xsdBase xsd:float).
---> (xsd:decimal rb:xsdBase xsd:decimal).
---> (xsd:string rb:xsdBase xsd:string).
---> (xsd:boolean rb:xsdBase xsd:boolean).
---> (xsd:date rb:xsdBase xsd:date).
---> (xsd:time rb:xsdBase xsd:time).
---> (xsd:dateTime rb:xsdBase xsd:dateTime).
---> (xsd:duration rb:xsdBase xsd:duration).
--
--# Describe range (base type, signed, min bits)
---> (xsd:byte rb:xsdRange xsd(xsd:integer,1,8)).
---> (xsd:short rb:xsdRange xsd(xsd:integer,1,16)).
---> (xsd:int rb:xsdRange xsd(xsd:integer,1,32)).
---> (xsd:long rb:xsdRange xsd(xsd:integer,1,64)).
---> (xsd:integer rb:xsdRange xsd(xsd:integer,1,65)).
--
---> (xsd:unsignedByte rb:xsdRange xsd(xsd:integer,0,8)).
---> (xsd:unsignedShort rb:xsdRange xsd(xsd:integer,0,16)).
---> (xsd:unsignedInt rb:xsdRange xsd(xsd:integer,0,32)).
---> (xsd:unsignedLong rb:xsdRange xsd(xsd:integer,0,64)).
---> (xsd:nonNegativeInteger rb:xsdRange xsd(xsd:integer,0,65)).
--
--# Some XSD support may be disabled temporarily during performance checking
--
--[xsd1: (?X rdfs:subClassOf ?Y) <-
-- (?X rb:xsdRange xsd(?B, 0, ?L)) (?Y rb:xsdRange xsd(?B, ?S, ?L2))
le(?L, ?L2)]
--
--[xsd2: (?X rdfs:subClassOf ?Y) <-
-- (?X rb:xsdRange xsd(?B, 1, ?L)) (?Y rb:xsdRange xsd(?B, 1, ?L2))
le(?L, ?L2)]
--
--[range2: (?P rdfs:range xsd:byte) <- (?P rdfs:range xsd:nonNegativeInteger),
-- (?P rdfs:range xsd:nonPositiveInteger)]
--
--[range3: (?P rdfs:range owl:Nothing) <- (?P rdfs:range ?C), (?P rdfs:range
?D), notEqual(?C, ?D)
-- (?C owl:disjointWith ?D) ]
--
--[xsd3: (?C owl:disjointWith ?D) <- (?C rb:xsdBase ?BC), (?D rb:xsdBase ?BD),
notEqual(?BC, ?BD) ]
--
--[range4: (?P rdfs:subPropertyOf ?Q) <- (?P rdfs:range owl:Nothing) (?Q
rdf:type rdf:Property)]
--
--
--#------------------------------------------------------------------
--# Validation rules. These are dormant by default but are triggered
--# by the additional of a validation control triple to the graph.
--#------------------------------------------------------------------
--
--[validationDomainMax0: (?v rb:validation on()), (?C rdfs:subClassOf max(?P,
0)), (?P rdfs:domain ?C) ->
-- (?P rb:violation error('inconsistent property definition', 'Property
defined with domain which has a max(0) restriction for that property (domain)',
?C) )
--]
--
--[validationMax0: (?v rb:validation on()), (?C rdfs:subClassOf max(?P, 0)) ->
-- [max2b: (?X rb:violation error('too many values', 'Value for max-0
property (prop, class)', ?P, ?C))
-- <- (?X rdf:type ?C), (?X ?P ?Y) ] ]
--
--[validationMaxN: (?v rb:validation on()), (?C rdfs:subClassOf max(?P, ?N)) ->
-- [max2b: (?X rb:violation error('too many values', 'Too many values on
max-N property (prop, class)', ?P, ?C))
-- <- (?X rdf:type ?C), countLiteralValues(?X, ?P, ?M), lessThan(?N,
?M) ] ]
--
--[validationFP: (?v rb:validation on()), (?P rdf:type owl:FunctionalProperty)
->
-- [fpb: (?X rb:violation error('too many values', 'Clashing literal values
for functional property', ?P, ?V, ?U))
-- <- (?X ?P ?V), countLiteralValues(?X, ?P, ?M), greaterThan(?M, 1) ]
]
--
--[validationMax1I: (?v rb:validation on()), (?C rdfs:subClassOf max(?P, 1))
(?P rdf:type owl:ObjectProperty) ->
-- [fpb: (?X rb:violation error('too many values', 'Clashing individual
values for card1 property', ?P, ?V, ?U))
-- <- (?X rdf:type ?C) (?X ?P ?V), (?X ?P ?U), notEqual(?V, ?U), (?U
owl:differentFrom ?V) ] ]
--
--[validationFPI: (?v rb:validation on()), (?P rdf:type owl:FunctionalProperty)
(?P rdf:type owl:ObjectProperty) ->
-- [fpb: (?X rb:violation error('too many values', 'Clashing individual
values for functional property', ?P, ?V, ?U))
-- <- (?X ?P ?V), (?X ?P ?U), notEqual(?V, ?U), (?U owl:differentFrom
?V) ] ]
--
--
--[validationIndiv: (?v rb:validation on()) ->
-- [validationIndiv: (?X rb:violation error('conflict', 'Two individuals both
same and different, may be due to disjoint classes or functional properties',
?Y))
-- <- (?X owl:differentFrom ?Y), (?X owl:sameAs ?Y), noValue(?T,
rb:prototype ?X) ] ]
--
--[validationIndiv2: (?v rb:validation on()) (?X owl:disjointWith ?Y) ->
-- [validationIndiv: (?I rb:violation error('conflict', 'Individual a member
of disjoint classes', ?X, ?Y))
-- <- (?I rdf:type ?X), (?I rdf:type ?Y) noValue(?T rb:prototype ?I)] ]
--
--[validationIndiv3: (?v rb:validation on()) ->
-- [validationIndiv: (?I rb:violation error('conflict', 'Individual a member
of Nothing', ?I))
-- <- (?I rdf:type owl:Nothing) noValue(?T rb:prototype ?I) ] ]
--
--[validationDisjoint: (?v rb:validation on()) (?X owl:disjointWith ?Y) ->
-- [validationIndiv: (?X rb:violation warn('Inconsistent class', 'Two classes
related by both subclass and disjoint relations', ?Y))
-- <- (?X owl:disjointWith ?Y), (?X rdfs:subClassOf ?Y) ] ]
--
--[validationDisjoint2: (?v rb:validation on()) (?X owl:disjointWith ?Y) ->
-- [validationIndiv: (?C rb:violation warn('Inconsistent class', 'subclass of
two disjoint classes', ?X, ?Y))
-- <- (?X owl:disjointWith ?Y), (?C rdfs:subClassOf ?X) (?C
rdfs:subClassOf ?Y) notEqual(?C, owl:Nothing) ] ]
--
--[validationDTP: (?v rb:validation on()), (?P rdf:type owl:DatatypeProperty) ->
-- [validationDTP: (?X rb:violation error('range check', 'Object value for
datatype property (prop, value)', ?P, ?V))
-- <- (?X ?P ?V), notLiteral(?V), notBNode(?V) ] ]
--
--[validationOP: (?v rb:validation on()), (?P rdf:type owl:ObjectProperty) ->
-- [validationDTP: (?X rb:violation warn('range check', 'Literal value for
object property (prop, value)', ?P, ?V))
-- <- (?X ?P ?V), isLiteral(?V) ] ]
--
--[validationDTRange: (?v rb:validation on()), (?P rdfs:range ?R) (?R rdf:type
rdfs:Datatype) ->
-- [validationDTRange: (?X rb:violation error('range check', 'Incorrectly
typed literal due to range (prop, value)', ?P, ?V))
-- <- (?X ?P ?V), notDType(?V, ?R) ] ]
--
--[validationDTRange: (?v rb:validation on()), (?P rdfs:range rdfs:Literal) ->
-- [validationDTRange: (?X rb:violation error('range check', 'Incorrectly
typed literal due to range rdsf:Literal (prop, value)', ?P, ?V))
-- <- (?X ?P ?V), notLiteral(?V), notBNode(?V) ] ]
--
--[validationAllFrom: (?v rb:validation on()), (?C rdfs:subClassOf all(?P, ?R))
(?R rdf:type rdfs:Datatype) ->
-- [validationDTRange: (?X rb:violation error('range check', 'Incorrectly
typed literal due to allValuesFrom (prop, value)', ?P, ?V))
-- <- (?X ?P ?V), (?X rdf:type ?C), notDType(?V, ?R) ] ]
--
--[validationAllFrom: (?v rb:validation on()), (?C owl:equivalentClass all(?P,
rdfs:Literal)) ->
-- [validationDTRange: (?X rb:violation error('range check', 'Incorrectly
typed literal due to allValuesFrom rdfs:Literal (prop, value)', ?P, ?V))
-- <- (?X ?P ?V), (?X rdf:type ?C), notDType(?V, rdfs:Literal)
-- ] ]
--
--[validationNothing: (?v rb:validation on()), (?C owl:equivalentClass
owl:Nothing) notEqual(?C, owl:Nothing) ->
-- (?C rb:violation warn('Inconsistent class', 'Class cannot be instantiated,
probably subclass of a disjoint classes or of an empty restriction'))
--]
--
--[validationRangeNothing: (?v rb:validation on()), (?P rdfs:range owl:Nothing)
->
-- (?C rb:violation warn('Inconsistent property', 'Property cannot be
instantiated, probably due to multiple disjoint range declarations'))
--]
--
--[validationOneOf: (?v rb:validation on()) (?C owl:oneOf ?L) ->
-- [validationIndiv: (?X rb:violation warn('possible oneof violation',
'Culprit is deduced to be of enumerated type (implicicated class) but is not
one of the enumerations\n This may be due to aliasing.', ?Y))
-- <- (?X rdf:type ?C), notBNode(?X), listNotContains(?L, ?X) ] ]
++# Licensed to the Apache Software Foundation (ASF) under one
++# or more contributor license agreements. See the NOTICE file
++# distributed with this work for additional information
++# regarding copyright ownership. The ASF licenses this file
++# to you under the Apache License, Version 2.0 (the
++# "License"); you may not use this file except in compliance
++# with the License. You may obtain a copy of the License at
++#
++# http://www.apache.org/licenses/LICENSE-2.0
++#
++# Unless required by applicable law or agreed to in writing, software
++# distributed under the License is distributed on an "AS IS" BASIS,
++# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
++# See the License for the specific language governing permissions and
++# limitations under the License.
++
++#------------------------------------------------------------------
++# OWL mini rule set v 0.1
++#
++# This is identical to the normal OWL rules except for:
++# - omit XSD range inheritance
++# - omit bNode introductin for someValuesFrom and minCardality
++#
++# $Id: owl-fb.rules,v 1.47 2004/03/09 18:36:30 der Exp $
++#------------------------------------------------------------------
++
++#------------------------------------------------------------------
++# Tabling directives
++#------------------------------------------------------------------
++
++-> tableAll().
++
++#-> table(rdf:type).
++#-> table(rdfs:subClassOf).
++#-> table(rdfs:range).
++#-> table(rdfs:domain).
++#-> table(owl:equivalentClass).
++
++#------------------------------------------------------------------
++# 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)]
++[rdf4: (?x ?p ?y) -> (?p rdf:type rdf:Property)]
++
++[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)]
++[rdfs5b: (?a rdfs:subPropertyOf ?a) <- (?a rdf:type rdf:Property)]
++[rdfs6: (?p rdfs:subPropertyOf ?q), notEqual(?p,?q) -> [ (?a ?q ?b) <- (?a
?p ?b)] ]
++[rdfs7: (?a rdf:type rdfs:Class) -> (?a rdfs:subClassOf ?a)]
++# omit rdfs8, derivable from rdfs9 and prototype2
++[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 ?z) <- bound(?x), (?x rdfs:domain ?y), (?y
rdfs:subClassOf ?z) ]
++[rdfs2a: (?x rdfs:domain ?z) <- unbound(?x), (?y rdfs:subClassOf ?z), (?x
rdfs:domain ?y) ]
++[rdfs3a: (?x rdfs:range ?z) <- bound(?x), (?x rdfs:range ?y), (?y
rdfs:subClassOf ?z) ]
++[rdfs3a: (?x rdfs:range ?z) <- unbound(?x), (?y rdfs:subClassOf ?z), (?x
rdfs:range ?y) ]
++
++[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)]
++
++[rdfsder1: (?p rdfs:range ?z) <- (?p rdfs:subPropertyOf ?q), notEqual(?p,
?q), (?q rdfs:range ?z)]
++[rdfsder2: (?p rdfs:domain ?z) <- (?p rdfs:subPropertyOf ?q), notEqual(?p,
?q), (?q rdfs:domain ?z)]
++
++#------------------------------------------------------------------
++# OWL axioms
++#------------------------------------------------------------------
++
++-> (owl:FunctionalProperty rdfs:subClassOf rdf:Property).
++-> (owl:ObjectProperty rdfs:subClassOf rdf:Property).
++-> (owl:DatatypeProperty rdfs:subClassOf rdf:Property).
++-> (owl:InverseFunctionalProperty rdfs:subClassOf owl:ObjectProperty).
++-> (owl:TransitiveProperty rdfs:subClassOf owl:ObjectProperty).
++-> (owl:SymmetricProperty rdfs:subClassOf owl:ObjectProperty).
++
++-> (rdf:first rdf:type owl:FunctionalProperty).
++-> (rdf:rest rdf:type owl:FunctionalProperty).
++
++-> (owl:oneOf rdfs:domain owl:Class).
++
++-> (owl:Class rdfs:subClassOf rdfs:Class).
++-> (owl:Restriction rdfs:subClassOf owl:Class).
++
++-> (owl:Thing rdf:type owl:Class).
++-> (owl:Nothing rdf:type owl:Class).
++
++-> (owl:equivalentClass rdfs:domain owl:Class).
++-> (owl:equivalentClass rdfs:range owl:Class).
++
++-> (owl:disjointWith rdfs:domain owl:Class).
++-> (owl:disjointWith rdfs:range owl:Class).
++
++-> (owl:sameAs rdf:type owl:SymmetricProperty).
++#-> (owl:sameIndividualAs owl:equivalentProperty owl:sameAs).
++
++# These are true but mess up the Ont API's notion of declared properties
++#-> (owl:sameAs rdfs:domain owl:Thing).
++#-> (owl:sameAs rdfs:range owl:Thing).
++#-> (owl:differentFrom rdfs:domain owl:Thing).
++#-> (owl:differentFrom rdfs:range owl:Thing).
++
++-> (owl:onProperty rdfs:domain owl:Restriction).
++-> (owl:onProperty rdfs:range owl:Property).
++
++-> (owl:OntologyProperty rdfs:subClassOf rdf:Property).
++-> (owl:imports rdf:type owl:OntologyProperty).
++-> (owl:imports rdfs:domain owl:Ontology).
++-> (owl:imports rdfs:range owl:Ontology).
++
++-> (owl:priorVersion rdfs:domain owl:Ontology).
++-> (owl:priorVersion rdfs:range owl:Ontology).
++
++-> (owl:backwardCompatibleWith rdfs:domain owl:Ontology).
++-> (owl:backwardCompatibleWith rdfs:range owl:Ontology).
++
++-> (owl:incompatibleWith rdfs:domain owl:Ontology).
++-> (owl:incompatibleWith rdfs:range owl:Ontology).
++
++-> (owl:versionInfo rdf:type owl:AnnotationProperty).
++
++# These properties are derivable from the definitions
++#-> (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:differentFrom rdf:type owl:SymmetricProperty).
++-> (owl:disjointWith rdf:type owl:SymmetricProperty).
++
++-> (owl:intersectionOf rdfs:domain owl:Class).
++
++#------------------------------------------------------------------
++# OWL Rules
++#------------------------------------------------------------------
++
++[thing1: (?C rdf:type owl:Class) -> (?C rdfs:subClassOf owl:Thing)]
++
++#------------------------------------------------------------------
++# One direction of unionOf
++#------------------------------------------------------------------
++
++[unionOf1: (?C owl:unionOf ?L) -> listMapAsSubject(?L, rdfs:subClassOf ?C) ]
++
++# Note could also add relation between two unionOf's if we add a listSubsumes
primitive
++
++#------------------------------------------------------------------
++# Prototype rules to convert instance reasoning to class subsumption checking
++#------------------------------------------------------------------
++
++[earlyTypeProp1: (?C rdf:type owl:Restriction) -> (?C rdf:type owl:Class) ]
++
++[earlyTypeProp2: (?C owl:intersectionOf ?X) -> (?C rdf:type owl:Class) ]
++
++[earlyTypeProp3: (?C rdf:type owl:Class) -> (?C rdf:type rdfs:Class) ]
++
++[prototype1: (?c rdf:type owl:Class), noValue(?c, rb:prototype), notEqual(?c,
owl:Nothing), makeTemp(?t), hide(?t)
++ -> (?c rb:prototype ?t), (?t rdf:type ?c) ]
++
++[prototype2: (?c rb:prototype ?p) ->
++ [prototype2b: (?c rdfs:subClassOf ?d) <- (?p rdf:type ?d)] ]
++
++#------------------------------------------------------------------
++# Identify restriction assertions
++#------------------------------------------------------------------
++
++[restriction1: (?C owl:onProperty ?P), (?C owl:someValuesFrom ?D)
++ -> (?C owl:equivalentClass some(?P, ?D))]
++
++[restriction2: (?C owl:onProperty ?P), (?C owl:allValuesFrom ?D)
++ -> (?C owl:equivalentClass all(?P, ?D))]
++
++[restriction3: (?C owl:onProperty ?P), (?C owl:minCardinality ?X)
++ -> (?C owl:equivalentClass min(?P, ?X))]
++
++[restriction4: (?C owl:onProperty ?P), (?C owl:maxCardinality ?X)
++ -> (?C owl:equivalentClass max(?P, ?X)) ]
++
++[restriction5: (?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))]
++
++# Could limit the work done here by inserting an isFunctor guard?
++[restrictionPropagate1: (?C owl:equivalentClass ?R), (?D rdfs:subClassOf ?C)
++ -> (?D rdfs:subClassOf ?R) ]
++[restrictionPropagate2: (?C owl:equivalentClass ?R), (?D owl:equivalentClass
?C)
++ -> (?D owl:equivalentClass ?R) ]
++
++# 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)] ]
++
++# This is redundant because equivalentClass is symmetric anyway
++#[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)]
++
++#------------------------------------------------------------------
++# min cardinality
++#------------------------------------------------------------------
++
++[minRec: (?C owl:equivalentClass min(?P, 1)), notEqual(?P, rdf:type) ->
++ [min2b: (?X rdf:type ?C) <- (?X ?P ?Y)] ]
++
++[restriction-inter-MnS: (?P rdfs:range ?D), (?C rdfs:subClassOf min(?P, 1))
++ -> (?C rdfs:subClassOf some(?P, ?D)) ]
++
++#------------------------------------------------------------------
++# max cardinality 1
++#------------------------------------------------------------------
++
++# Rule move to sameInstance block below to ease experimentation
++#[max1: (?C rdfs:subClassOf max(?P, 1)) ->
++# [max1b: (?Y1 owl:sameAs ?Y2) <- bound(?Y1), (?X ?P ?Y1), (?X rdf:type
?C), (?X ?P ?Y2), notEqual(?Y1, ?Y2)]
++# [max1b: (?Y1 owl:sameAs ?Y2) <- unbound(?Y1), (?X ?P ?Y2), (?X rdf:type
?C), (?X ?P ?Y1), notEqual(?Y1, ?Y2)]
++# ]
++
++[maxRec: (?C owl:equivalentClass max(?P, 1)), (?P rdf:type
owl:FunctionalProperty) ->
++ [ (?X rdf:type ?C) <- (?X rdf:type owl:Thing)] ]
++
++#------------------------------------------------------------------
++# max cardinality 0
++#------------------------------------------------------------------
++
++# For completeness this requires iff version of rdfs:domain working forwards
which it does not just now
++[maxRec2: (?C owl:equivalentClass max(?P, 0)), (?P rdfs:domain ?D), (?E
owl:disjointWith ?D)
++ -> (?E rdfs:subClassOf ?C)]
++
++[cardRec1: (?C owl:equivalentClass card(?P, 0)), (?P rdfs:domain ?D), (?E
owl:disjointWith ?D)
++ -> (?E rdfs:subClassOf ?C)]
++
++[cardRec3: (?C owl:equivalentClass card(?P, 0)) ->
++ [cardRec2b: (?X rdf:type ?C) <- (?X rdf:type max(?P, 0))] ]
++
++#------------------------------------------------------------------
++# cardinality 1
++#------------------------------------------------------------------
++
++[restriction-inter-CFP: (?C owl:equivalentClass card(?P, 1)), (?P rdf:type
owl:FunctionalProperty) ->
++ (?C owl:equivalentClass min(?P, 1)) ]
++
++[cardRec2: (?C owl:equivalentClass card(?P, 1)) ->
++ [cardRec2b: (?X rdf:type ?C) <- (?X rdf:type min(?P, 1)), (?X rdf:type
max(?P, 1)) ] ]
++
++#------------------------------------------------------------------
++# someValuesFrom
++#------------------------------------------------------------------
++
++#[someRec: (?C owl:equivalentClass some(?P, ?D)), (?P rdfs:range ?D) ->
++# [someRecb: (?X rdf:type ?C) <- (?X ?P ?A) ] ]
++
++[someRec2: (?C owl:equivalentClass some(?P, ?D)) ->
++ [someRec2b: (?X rdf:type ?C) <- (?X ?P ?A) (?A rdf:type ?D) ] ]
++
++[someRec2b: (?C owl:equivalentClass some(?P, ?D)), (?D rdf:type
rdfs:Datatype)->
++ [someRec2b: (?X rdf:type ?C) <- (?X ?P ?A), isDType(?A, ?D) ] ]
++
++#------------------------------------------------------------------
++# allValuesFrom
++#------------------------------------------------------------------
++
++[all1: (?C rdfs:subClassOf all(?P, ?D)), notEqual(?P, rdf:type), notEqual(?C,
?D) ->
++ [all1b: (?Y rdf:type ?D) <- (?X ?P ?Y), (?X rdf:type ?C) ] ]
++
++[allRec1: (?C rdfs:subClassOf max(?P, 1)), (?C rdfs:subClassOf some(?P, ?D))
++ -> (?C rdfs:subClassOf all(?P, ?D)) ]
++
++[allRec2: (?P rdf:type owl:FunctionalProperty), (?C rdfs:subClassOf some(?P,
?C))
++ -> (?C rdfs:subClassOf all(?P, ?C)) ]
++
++[allRec3: (?C owl:equivalentClass all(?P, ?D)), (?P rdfs:range ?D) ->
++ [ (?X rdf:type ?C) <- (?X rdf:type owl:Thing)] ]
++
++[allRec4: (?P rdf:type owl:FunctionalProperty), (?C owl:equivalentClass
all(?P, ?D))
++ -> [ (?X rdf:type ?C) <- (?X ?P ?Y) (?Y rdf:type ?D)
] ]
++
++[allRec5: (?C rdfs:subClassOf max(?P, 1)) (?C owl:equivalentClass all(?P, ?D))
++ -> [ (?X rdf:type ?C) <- (?X ?P ?Y) (?Y rdf:type ?D)
] ]
++
++[restriction-inter-RA-T: (?P rdfs:range ?C), (?D owl:equivalentClass all(?P,
?C))
++ -> (owl:Thing rdfs:subClassOf ?D) ]
++
++[restriction-inter-AT-R: (owl:Thing rdfs:subClassOf all(?P, ?C))
++ -> (?P rdfs:range ?C), (?P rdf:type owl:ObjectProperty) ]
++
++# This version looks strange but we are experimenting with droping the direct
++# subclass transitive closure and inferring from prototypes, but that is being
++# done backwards for forwards subclass relationships are handled as special
cases
++#[restriction-inter-AT-R: (owl:Thing rdfs:subClassOf ?D) (?D
owl:equivalentClass all(?P, ?C))
++# -> (?P rdfs:range ?C), (?P
rdf:type owl:ObjectProperty) ]
++
++#------------------------------------------------------------------
++# Nothing
++#------------------------------------------------------------------
++
++[nothing1: (?C rdfs:subClassOf min(?P, ?n)) (?C rdfs:subClassOf max(?P, ?x))
++ lessThan(?x, ?n) -> (?C owl:equivalentClass owl:Nothing) ]
++
++[nothing2: (?C rdfs:subClassOf ?D) (?C rdfs:subClassOf ?E) (?D
owl:disjointWith ?E)
++ -> (?C owl:equivalentClass owl:Nothing) ]
++
++[nothing3: (?C rdfs:subClassOf owl:Nothing) -> (?C owl:equivalentClass
owl:Nothing) ]
++
++[nothing4: (?C owl:oneOf rdf:nil) -> (?C owl:equivalentClass owl:Nothing) ]
++
++#------------------------------------------------------------------
++# Disjointness
++#------------------------------------------------------------------
++
++#[distinct1: (?C owl:disjointWith ?D), (?X rdf:type ?C), (?Y rdf:type ?D)
++# -> (?X owl:differentFrom ?Y) ]
++
++[distinct1: (?X owl:differentFrom ?Y) <-
++ (?C owl:disjointWith ?D), (?X rdf:type ?C), (?Y rdf:type ?D) ]
++
++# 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) ]
++
++#------------------------------------------------------------------
++# Class equality
++#------------------------------------------------------------------
++
++# equivalentClass
++[equivalentClass1: (?P owl:equivalentClass ?Q)
++ -> (?P rdfs:subClassOf ?Q), (?Q rdfs:subClassOf ?P) ]
++
++[equivalentClass2: (?P owl:equivalentClass ?Q) <- (?P rdfs:subClassOf ?Q),
(?Q rdfs:subClassOf ?P) ]
++
++[equivalentClass3: (?P owl:sameAs ?Q), (?P rdf:type rdfs:Class), (?Q rdf:type
rdfs:Class)
++ -> (?P owl:equivalentClass ?Q) ]
++
++#------------------------------------------------------------------
++# Instance equality
++#------------------------------------------------------------------
++
++# sameAs
++
++#[sameAs1: (?P rdf:type owl:FunctionalProperty) ->
++# [sameAs1b: (?B owl:sameAs ?C) <- unbound(?C), (?A ?P ?B), (?A ?P ?C) ]
++# [sameAs1b: (?B owl:sameAs ?C) <- bound(?C), (?A ?P ?C), (?A ?P ?B) ]
++# ]
++#
++#[sameAs2: (?P rdf:type owl:InverseFunctionalProperty) ->
++# [sameAs2b: (?A owl:sameAs ?C) <- unbound(?C), (?A ?P ?B), (?C ?P ?B) ]
++# [sameAs2b: (?A owl:sameAs ?C) <- bound(?C), (?C ?P ?B), (?A ?P ?B) ]
++# ]
++#
++##[sameAs3: (?X owl:sameAs ?Y), (?X rdf:type owl:Thing), (?Y rdf:type
owl:Thing)
++## -> (?X owl:sameAs ?Y) ]
++#
++#[sameAs4a: (?Y ?P ?V) <- unbound(?V), (?X owl:sameAs ?Y), notEqual(?X,?Y),
(?X ?P ?V) ]
++#[sameAs4c: (?Y ?P ?V) <- bound(?V), (?X ?P ?V), notEqual(?X,?Y), (?X
owl:sameAs ?Y) ]
++#[sameAs5a: (?V ?P ?Y) <- unbound(?V), (?X owl:sameAs ?Y), notEqual(?X,?Y),
(?V ?P ?X) ]
++#[sameAs5c: (?V ?P ?Y) <- bound(?V), (?V ?P ?X), notEqual(?X,?Y), (?X
owl:sameAs ?Y) ]
++#
++#[sameAs6: (?X rdf:type owl:Thing) <- (?X owl:sameAs ?Y) ]
++##[sameAs6: (?Y rdf:type owl:Thing) <- (?X owl:sameAs ?Y) ]
++
++#------------------------------------------------------------------
++# Experimental forward version of instance equality
++#------------------------------------------------------------------
++
++# sameAs recognition rules - forward version
++
++[fp1: (?P rdf:type owl:FunctionalProperty), (?A ?P ?B), notLiteral(?B), (?A
?P ?C), notLiteral(?C)
++ notEqual(?B, ?C) -> (?B owl:sameAs ?C) ]
++
++[ifp1: (?P rdf:type owl:InverseFunctionalProperty), (?A ?P ?B), (?C ?P ?B)
++ notEqual(?A, ?C) -> (?A owl:sameAs ?C) ]
++
++[fp1: (?P rdf:type owl:FunctionalProperty), (?A ?P ?B), notLiteral(?B), (?A
?Q ?C), notLiteral(?C),
++ notEqual(?B, ?C), (?Q rdfs:subPropertyOf ?P) -> (?B owl:sameAs ?C) ]
++
++[ifp1: (?P rdf:type owl:InverseFunctionalProperty), (?A ?P ?B), (?C ?Q ?B)
++ notEqual(?A, ?C), (?Q rdfs:subPropertyOf ?P) -> (?A owl:sameAs ?C)
]
++
++[fpEarlyProp: (?P rdf:type owl:FunctionalProperty) (?Q rdfs:subPropertyOf ?P)
->
++ (?Q rdf:type owl:FunctionalProperty) ]
++
++[ifpEarlyProp: (?P rdf:type owl:InverseFunctionalProperty) (?Q
rdfs:subPropertyOf ?P) ->
++ (?Q rdf:type owl:InverseFunctionalProperty) ]
++
++# This rule is not sufficient if the type inference is being done backwards
++[max1: (?C rdfs:subClassOf max(?P, 1)), (?X ?P ?Y1), notLiteral(?Y1), (?X
rdf:type ?C), (?X ?P ?Y2), notLiteral(?Y2),
++ notEqual(?Y1, ?Y2) -> (?Y1 owl:sameAs ?Y2) ]
++
++# Subclass inheritance not normally availabe forward which causes problems
for max1,
++# patch this but just for restrictions to limit costs
++[subClassTemp: (?C rdfs:subClassOf ?R), isFunctor(?R), (?B rdfs:subClassOf
?C) -> (?B rdfs:subClassOf ?R) ]
++
++# sameAs propagation rules - forward version
++
++[sameAs1: (?A owl:sameAs ?B) -> (?B owl:sameAs ?A) ]
++
++[sameAs2: (?A owl:sameAs ?B) (?B owl:sameAs ?C) -> (?A owl:sameAs ?C) ]
++
++[sameAs6: (?X rdf:type owl:Thing) <- (?X owl:sameAs ?Y) ]
++
++# Was
++# [sameAs7: (?X owl:sameAs ?X) <- bound(?X) (?X rdf:type owl:Thing) ]
++# which is not complete and breaks the find() contract.
++# Investigate why I though this was a useful thing to do in the first place!
++[sameAs7: (?X owl:sameAs ?X) <- (?X rdf:type owl:Thing) ]
++
++# Equality processing rules
++
++[equality1: (?X owl:sameAs ?Y), notEqual(?X,?Y) ->
++ [(?X ?P ?V) <- (?Y ?P ?V)]
++ [(?V ?P ?X) <- (?V ?P ?Y)] ]
++
++[equality2: (?X owl:sameAs ?Y), (?X rdf:type owl:Class) -> (?X
owl:equivalentClass ?Y) ]
++
++[equality3: (?X owl:sameAs ?Y), (?X rdf:type rdf:Property) -> (?X
owl:equivalentProperty ?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 rdfs:Property), (?Q
rdf:type rdfs:Property)
++ -> (?P owl:equivalentProperty ?Q) ]
++
++# SymmetricProperty
++
++[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) -> [inverseOf2b: (?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) ]
++
++[inverseof5: (?P owl:inverseOf ?Q) (?P rdfs:range ?C) -> (?Q rdfs:domain ?C)]
++[inverseof6: (?P owl:inverseOf ?Q) (?P rdfs:domain ?C) -> (?Q rdfs:range ?C)]
++
++# TransitiveProperty
++
++[transitiveProperty1: (?P rdf:type owl:TransitiveProperty) ->
++# [transitiveProperty1b: (?A ?P ?C) <- (?A ?P ?B), (?B
?P ?C)] ]
++ [transitiveProperty1b: (?A ?P ?C) <- bound (?C), (?B ?P ?C), (?A ?P
?B)]
++ [transitiveProperty1b: (?A ?P ?C) <- unbound (?C), (?A ?P ?B) (?B ?P
?C)]
++ ]
++
++# Object properties
++
++[objectProperty: (?P rdf:type owl:ObjectProperty) ->
++ (?P rdfs:domain owl:Thing) (?P rdfs:range owl:Thing) ]
++
++#------------------------------------------------------------------
++# Restricted support for hasValue, even though that is beyond OWL/lite
++#------------------------------------------------------------------
++
++# hasValue
++[hasValueRec: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C
owl:hasValue ?V)
++ -> (?C owl:equivalentClass hasValue(?P, ?V)) ]
++
++[hasValueIF: (?C owl:equivalentClass hasValue(?P, ?V)) ->
++ [ (?x ?P ?V) <- (?x rdf:type ?C) ]
++ [ (?x rdf:type ?C) <- (?x ?P ?V) ]
++ ]
++
++[hasValueProp: (?P rdf:type owl:FunctionalProperty) (?Q rdf:type
owl:FunctionalProperty)
++ (?P rdfs:domain ?D) (?Q rdfs:domain ?D)
++ (?D owl:equivalentClass hasValue(?P, ?V))
++ (?D owl:equivalentClass hasValue(?Q, ?V))
++ -> (?P owl:equivalentProperty ?Q)]
++
++
++#------------------------------------------------------------------
++# Restricted support for oneOf, even though that is beyond OWL/lite
++#------------------------------------------------------------------
++
++[oneOfFP: (?P rdfs:range ?C) (?C owl:oneOf ?l) (?l rdf:first ?x) (?l rdf:rest
rdf:nil)
++ -> (?P rdf:type owl:FunctionalProperty) ]
++
++[oneOfIFP: (?P rdfs:domain ?C) (?C owl:oneOf ?l) (?l rdf:first ?x) (?l
rdf:rest rdf:nil)
++ -> (?P rdf:type owl:InverseFunctionalProperty) ]
++
++[oneOf1: (?C owl:oneOf ?l) -> listMapAsSubject(?l, rdf:type, ?C) ]
++
++[oneOf2: (?C owl:oneOf ?l1) (?D owl:oneOf ?l2) notEqual(?l1, ?l2)
listEqual(?l1, ?l2) -> (?C owl:equivalentClass ?D) ]
++
++[oneOf3: (?C owl:oneOf ?l) (?l rdf:first ?x) (?l rdf:rest rdf:nil) ->
++ [ (?Y ?P ?x) <- (?Y ?P ?I) (?I rdf:type ?C) ] ]
++
++#------------------------------------------------------------------
++# Declaration of main XSD datatypes
++#------------------------------------------------------------------
++
++-> (xsd:float rdf:type rdfs:Datatype).
++-> (xsd:double rdf:type rdfs:Datatype).
++-> (xsd:int rdf:type rdfs:Datatype).
++-> (xsd:long rdf:type rdfs:Datatype).
++-> (xsd:short rdf:type rdfs:Datatype).
++-> (xsd:byte rdf:type rdfs:Datatype).
++-> (xsd:unsignedByte rdf:type rdfs:Datatype).
++-> (xsd:unsignedShort rdf:type rdfs:Datatype).
++-> (xsd:unsignedInt rdf:type rdfs:Datatype).
++-> (xsd:unsignedLong rdf:type rdfs:Datatype).
++-> (xsd:decimal rdf:type rdfs:Datatype).
++-> (xsd:integer rdf:type rdfs:Datatype).
++-> (xsd:nonPositiveInteger rdf:type rdfs:Datatype).
++-> (xsd:nonNegativeInteger rdf:type rdfs:Datatype).
++-> (xsd:positiveInteger rdf:type rdfs:Datatype).
++-> (xsd:negativeInteger rdf:type rdfs:Datatype).
++-> (xsd:boolean rdf:type rdfs:Datatype).
++-> (xsd:string rdf:type rdfs:Datatype).
++-> (xsd:anyURI rdf:type rdfs:Datatype).
++-> (xsd:hexBinary rdf:type rdfs:Datatype).
++-> (xsd:base64Binary rdf:type rdfs:Datatype).
++-> (xsd:date rdf:type rdfs:Datatype).
++-> (xsd:time rdf:type rdfs:Datatype).
++-> (xsd:dateTime rdf:type rdfs:Datatype).
++-> (xsd:duration rdf:type rdfs:Datatype).
++-> (xsd:gDay rdf:type rdfs:Datatype).
++-> (xsd:gMonth rdf:type rdfs:Datatype).
++-> (xsd:gYear rdf:type rdfs:Datatype).
++-> (xsd:gYearMonth rdf:type rdfs:Datatype).
++-> (xsd:gMonthDay rdf:type rdfs:Datatype).
++
++-> (xsd:integer rdfs:subClassOf xsd:decimal).
++
++-> hide(rb:xsdBase).
++-> hide(rb:xsdRange).
++-> hide(rb:prototype).
++
++-> (xsd:byte rb:xsdBase xsd:decimal).
++-> (xsd:short rb:xsdBase xsd:decimal).
++-> (xsd:int rb:xsdBase xsd:decimal).
++-> (xsd:long rb:xsdBase xsd:decimal).
++-> (xsd:unsignedByte rb:xsdBase xsd:decimal).
++-> (xsd:unsignedShort rb:xsdBase xsd:decimal).
++-> (xsd:unsignedInt rb:xsdBase xsd:decimal).
++-> (xsd:unsignedLong rb:xsdBase xsd:decimal).
++-> (xsd:integer rb:xsdBase xsd:decimal).
++-> (xsd:nonNegativeInteger rb:xsdBase xsd:decimal).
++-> (xsd:nonPositiveInteger rb:xsdBase xsd:decimal).
++-> (xsd:byte rb:xsdBase xsd:decimal).
++-> (xsd:float rb:xsdBase xsd:float).
++-> (xsd:decimal rb:xsdBase xsd:decimal).
++-> (xsd:string rb:xsdBase xsd:string).
++-> (xsd:boolean rb:xsdBase xsd:boolean).
++-> (xsd:date rb:xsdBase xsd:date).
++-> (xsd:time rb:xsdBase xsd:time).
++-> (xsd:dateTime rb:xsdBase xsd:dateTime).
++-> (xsd:duration rb:xsdBase xsd:duration).
++
++# Describe range (base type, signed, min bits)
++-> (xsd:byte rb:xsdRange xsd(xsd:integer,1,8)).
++-> (xsd:short rb:xsdRange xsd(xsd:integer,1,16)).
++-> (xsd:int rb:xsdRange xsd(xsd:integer,1,32)).
++-> (xsd:long rb:xsdRange xsd(xsd:integer,1,64)).
++-> (xsd:integer rb:xsdRange xsd(xsd:integer,1,65)).
++
++-> (xsd:unsignedByte rb:xsdRange xsd(xsd:integer,0,8)).
++-> (xsd:unsignedShort rb:xsdRange xsd(xsd:integer,0,16)).
++-> (xsd:unsignedInt rb:xsdRange xsd(xsd:integer,0,32)).
++-> (xsd:unsignedLong rb:xsdRange xsd(xsd:integer,0,64)).
++-> (xsd:nonNegativeInteger rb:xsdRange xsd(xsd:integer,0,65)).
++
++# Some XSD support may be disabled temporarily during performance checking
++
++[xsd1: (?X rdfs:subClassOf ?Y) <-
++ (?X rb:xsdRange xsd(?B, 0, ?L)) (?Y rb:xsdRange xsd(?B, ?S, ?L2))
le(?L, ?L2)]
++
++[xsd2: (?X rdfs:subClassOf ?Y) <-
++ (?X rb:xsdRange xsd(?B, 1, ?L)) (?Y rb:xsdRange xsd(?B, 1, ?L2))
le(?L, ?L2)]
++
++[range2: (?P rdfs:range xsd:byte) <- (?P rdfs:range xsd:nonNegativeInteger),
++ (?P rdfs:range xsd:nonPositiveInteger)]
++
++[range3: (?P rdfs:range owl:Nothing) <- (?P rdfs:range ?C), (?P rdfs:range
?D), notEqual(?C, ?D)
++ (?C owl:disjointWith ?D) ]
++
++[xsd3: (?C owl:disjointWith ?D) <- (?C rb:xsdBase ?BC), (?D rb:xsdBase ?BD),
notEqual(?BC, ?BD) ]
++
++[range4: (?P rdfs:subPropertyOf ?Q) <- (?P rdfs:range owl:Nothing) (?Q
rdf:type rdf:Property)]
++
++
++#------------------------------------------------------------------
++# Validation rules. These are dormant by default but are triggered
++# by the additional of a validation control triple to the graph.
++#------------------------------------------------------------------
++
++[validationDomainMax0: (?v rb:validation on()), (?C rdfs:subClassOf max(?P,
0)), (?P rdfs:domain ?C) ->
++ (?P rb:violation error('inconsistent property definition', 'Property
defined with domain which has a max(0) restriction for that property (domain)',
?C) )
++]
++
++[validationMax0: (?v rb:validation on()), (?C rdfs:subClassOf max(?P, 0)) ->
++ [max2b: (?X rb:violation error('too many values', 'Value for max-0
property (prop, class)', ?P, ?C))
++ <- (?X rdf:type ?C), (?X ?P ?Y) ] ]
++
++[validationMaxN: (?v rb:validation on()), (?C rdfs:subClassOf max(?P, ?N)) ->
++ [max2b: (?X rb:violation error('too many values', 'Too many values on
max-N property (prop, class)', ?P, ?C))
++ <- (?X rdf:type ?C), countLiteralValues(?X, ?P, ?M), lessThan(?N,
?M) ] ]
++
++[validationFP: (?v rb:validation on()), (?P rdf:type owl:FunctionalProperty)
->
++ [fpb: (?X rb:violation error('too many values', 'Clashing literal values
for functional property', ?P, ?V, ?U))
++ <- (?X ?P ?V), countLiteralValues(?X, ?P, ?M), greaterThan(?M, 1) ]
]
++
++[validationMax1I: (?v rb:validation on()), (?C rdfs:subClassOf max(?P, 1))
(?P rdf:type owl:ObjectProperty) ->
++ [fpb: (?X rb:violation error('too many values', 'Clashing individual
values for card1 property', ?P, ?V, ?U))
++ <- (?X rdf:type ?C) (?X ?P ?V), (?X ?P ?U), notEqual(?V, ?U), (?U
owl:differentFrom ?V) ] ]
++
++[validationFPI: (?v rb:validation on()), (?P rdf:type owl:FunctionalProperty)
(?P rdf:type owl:ObjectProperty) ->
++ [fpb: (?X rb:violation error('too many values', 'Clashing individual
values for functional property', ?P, ?V, ?U))
++ <- (?X ?P ?V), (?X ?P ?U), notEqual(?V, ?U), (?U owl:differentFrom
?V) ] ]
++
++
++[validationIndiv: (?v rb:validation on()) ->
++ [validationIndiv: (?X rb:violation error('conflict', 'Two individuals both
same and different, may be due to disjoint classes or functional properties',
?Y))
++ <- (?X owl:differentFrom ?Y), (?X owl:sameAs ?Y), noValue(?T,
rb:prototype ?X) ] ]
++
++[validationIndiv2: (?v rb:validation on()) (?X owl:disjointWith ?Y) ->
++ [validationIndiv: (?I rb:violation error('conflict', 'Individual a member
of disjoint classes', ?X, ?Y))
++ <- (?I rdf:type ?X), (?I rdf:type ?Y) noValue(?T rb:prototype ?I)] ]
++
++[validationIndiv3: (?v rb:validation on()) ->
++ [validationIndiv: (?I rb:violation error('conflict', 'Individual a member
of Nothing', ?I))
++ <- (?I rdf:type owl:Nothing) noValue(?T rb:prototype ?I) ] ]
++
++[validationDisjoint: (?v rb:validation on()) (?X owl:disjointWith ?Y) ->
++ [validationIndiv: (?X rb:violation warn('Inconsistent class', 'Two classes
related by both subclass and disjoint relations', ?Y))
++ <- (?X owl:disjointWith ?Y), (?X rdfs:subClassOf ?Y) ] ]
++
++[validationDisjoint2: (?v rb:validation on()) (?X owl:disjointWith ?Y) ->
++ [validationIndiv: (?C rb:violation warn('Inconsistent class', 'subclass of
two disjoint classes', ?X, ?Y))
++ <- (?X owl:disjointWith ?Y), (?C rdfs:subClassOf ?X) (?C
rdfs:subClassOf ?Y) notEqual(?C, owl:Nothing) ] ]
++
++[validationDTP: (?v rb:validation on()), (?P rdf:type owl:DatatypeProperty) ->
++ [validationDTP: (?X rb:violation error('range check', 'Object value for
datatype property (prop, value)', ?P, ?V))
++ <- (?X ?P ?V), notLiteral(?V), notBNode(?V) ] ]
++
++[validationOP: (?v rb:validation on()), (?P rdf:type owl:ObjectProperty) ->
++ [validationDTP: (?X rb:violation warn('range check', 'Literal value for
object property (prop, value)', ?P, ?V))
++ <- (?X ?P ?V), isLiteral(?V) ] ]
++
++[validationDTRange: (?v rb:validation on()), (?P rdfs:range ?R) (?R rdf:type
rdfs:Datatype) ->
++ [validationDTRange: (?X rb:violation error('range check', 'Incorrectly
typed literal due to range (prop, value)', ?P, ?V))
++ <- (?X ?P ?V), notDType(?V, ?R) ] ]
++
++[validationDTRange: (?v rb:validation on()), (?P rdfs:range rdfs:Literal) ->
++ [validationDTRange: (?X rb:violation error('range check', 'Incorrectly
typed literal due to range rdsf:Literal (prop, value)', ?P, ?V))
++ <- (?X ?P ?V), notLiteral(?V), notBNode(?V) ] ]
++
++[validationAllFrom: (?v rb:validation on()), (?C rdfs:subClassOf all(?P, ?R))
(?R rdf:type rdfs:Datatype) ->
++ [validationDTRange: (?X rb:violation error('range check', 'Incorrectly
typed literal due to allValuesFrom (prop, value)', ?P, ?V))
++ <- (?X ?P ?V), (?X rdf:type ?C), notDType(?V, ?R) ] ]
++
++[validationAllFrom: (?v rb:validation on()), (?C owl:equivalentClass all(?P,
rdfs:Literal)) ->
++ [validationDTRange: (?X rb:violation error('range check', 'Incorrectly
typed literal due to allValuesFrom rdfs:Literal (prop, value)', ?P, ?V))
++ <- (?X ?P ?V), (?X rdf:type ?C), notDType(?V, rdfs:Literal)
++ ] ]
++
++[validationNothing: (?v rb:validation on()), (?C owl:equivalentClass
owl:Nothing) notEqual(?C, owl:Nothing) ->
++ (?C rb:violation warn('Inconsistent class', 'Class cannot be instantiated,
probably subclass of a disjoint classes or of an empty restriction'))
++]
++
++[validationRangeNothing: (?v rb:validation on()), (?P rdfs:range owl:Nothing)
->
++ (?C rb:violation warn('Inconsistent property', 'Property cannot be
instantiated, probably due to multiple disjoint range declarations'))
++]
++
++[validationOneOf: (?v rb:validation on()) (?C owl:oneOf ?L) ->
++ [validationIndiv: (?X rb:violation warn('possible oneof violation',
'Culprit is deduced to be of enumerated type (implicicated class) but is not
one of the enumerations\n This may be due to aliasing.', ?Y))
++ <- (?X rdf:type ?C), notBNode(?X), listNotContains(?L, ?X) ] ]
