You are viewing a plain text version of this content. The canonical link for it is here.
Posted to commits@jena.apache.org by an...@apache.org on 2016/05/14 14:03:29 UTC

[30/42] jena git commit: Merge commit 'refs/pull/143/head' of github.com:apache/jena

http://git-wip-us.apache.org/repos/asf/jena/blob/4b5cd267/jena-core/src/main/resources/etc/owl-fb-micro.rules
----------------------------------------------------------------------
diff --cc jena-core/src/main/resources/etc/owl-fb-micro.rules
index 9e87ef5,9e87ef5..b2f8488
--- a/jena-core/src/main/resources/etc/owl-fb-micro.rules
+++ b/jena-core/src/main/resources/etc/owl-fb-micro.rules
@@@ -1,582 -1,582 +1,582 @@@
--# 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 micro rule set v0.1
--# This rule set is designed to implement owl(f)lite using the hybrid
--# rule system (mixture of forward and backward chaining).
--#
--# This differs from the normal OWL rule set in several ways.
--#  - no equality reasoning (sameAs, FunctionalProperty ...)
--#  - omits the someValuesFrom => bNode entailments.
--#  - avoids any guard clauses which would break the find() contract.
--#  - TGC for subClass hierarchies, all subClassOf derivations are forward.
--#  - omits use of prototypes and relies on explicit rules for subClassOf 
--#    derivations this may lead to additional incompletenesses
--#
--# $Id: owl-fb.rules,v 1.45 2004/03/02 13:38:53 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
--#------------------------------------------------------------------
--
--[rdf1and4: (?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)] ] 
--[rdfs5b: (?a rdf:type rdf:Property) -> (?a rdfs:subPropertyOf ?a)] 
--[rdfs6:  (?p rdfs:subPropertyOf ?q), notEqual(?p,?q) -> table(?p, ?q), [ (?a ?q ?b) <- (?a ?p ?b)] ] 
--[rdfs7:  (?a rdf:type rdfs:Class) -> (?a rdfs:subClassOf ?a)]
--[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)]
--
--[rdfs9-alt:  (?a rdf:type ?y) <- bound(?y) (?x rdfs:subClassOf ?y), (?a rdf:type ?x) ] 
--[rdfs9-alt:  (?a rdf:type ?y) <- unbound(?y) (?a rdf:type ?x) (?x rdfs:subClassOf ?y) ] 
--
--#------------------------------------------------------------------
--# 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).
--
--# 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), (owl:Nothing rdfs:subClassOf ?C)]
--
--#------------------------------------------------------------------
--# 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 owl:Class), (?Q rdf:type owl:Class) 
--						-> (?P owl:equivalentClass ?Q) ]
--		
--#------------------------------------------------------------------
--# 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) ]
--
--# SymmetricProperty
--
--[symmetricProperty1: (?P rdf:type owl:SymmetricProperty) -> table(?P),
--                     [symmetricProperty1b: (?X ?P ?Y) <- (?Y ?P ?X)] ]
--
--
--# inverseOf
--[inverseOf1: (?P owl:inverseOf ?Q) -> (?Q owl:inverseOf ?P) ]
--
--[inverseOf2: (?P owl:inverseOf ?Q) -> table(?P), table(?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) -> table(?P),
--#			[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) ]
--						
--#------------------------------------------------------------------
--# 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)).
--
--#------------------------------------------------------------------
--# 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))]
--       					
--[hasValueRec: (?C owl:onProperty ?P), (?C owl:hasValue ?V)
--	-> (?C owl:equivalentClass hasValue(?P, ?V)) ]
--						
--
--## TODO do we need the early restriction propagation rules in this configuration?
--
--# Equality propagation
--
--[restrictionEq1: (?R1 owl:equivalentClass some(?P, ?C)) (?R2 owl:equivalentClass some(?P, ?C))
--					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
--[restrictionEq2: (?R1 owl:equivalentClass all(?P, ?C)) (?R2 owl:equivalentClass all(?P, ?C))
--					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
--[restrictionEq3: (?R1 owl:equivalentClass min(?P, ?C)) (?R2 owl:equivalentClass min(?P, ?C))
--					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
--[restrictionEq4: (?R1 owl:equivalentClass max(?P, ?C)) (?R2 owl:equivalentClass max(?P, ?C))
--					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
--[restrictionEq5: (?R1 owl:equivalentClass card(?P, ?C)) (?R2 owl:equivalentClass card(?P, ?C))
--					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
--[restrictionEq6: (?R1 owl:equivalentClass hasValue(?P, ?C)) (?R2 owl:equivalentClass hasValue(?P, ?C))
--					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
--					
--#[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) ]
--
--
--#------------------------------------------------------------------
--# 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
--
--#------------------------------------------------------------------
--# Intersection of (instance reasoning is done by the translation hook)
--#------------------------------------------------------------------
--
--[intersectionOf1:  (?C owl:intersectionOf ?L) -> listMapAsObject(?C rdfs:subClassOf ?L) ]
--
--#------------------------------------------------------------------
--# someValuesFrom - recognition direction only
--#------------------------------------------------------------------
--    
--[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) ] ]
--
--# In the absence of prototype and bNode introduction rules we have to manually
--# code in additional subclass relationships
--
--[restriction-inter-MnS: (?P rdfs:range ?D), (?C rdfs:subClassOf min(?P, 1)) 
--						-> (?C rdfs:subClassOf some(?P, ?D)) ]
--						
--#------------------------------------------------------------------
--# allValuesFrom (main rule is in Mini, this just does minimal subclass propagation
--#------------------------------------------------------------------
--
--[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)) ]
--    
--[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) ]
--						
--#------------------------------------------------------------------
--# Restricted support for hasValue, even though that is beyond OWL/lite
--#------------------------------------------------------------------
--
--# hasValue
--[hasValueIF: (?C owl:equivalentClass hasValue(?P, ?V)) -> 
--								[ (?x ?P ?V) <- (?x rdf:type ?C) ]
--								[ (?x rdf:type ?C) <- (?x ?P ?V) ]
--								]
--
--#------------------------------------------------------------------
--# Nothing
--#------------------------------------------------------------------
--    
--[nothing1: (?C rdfs:subClassOf min(?P, ?n)) (?C rdfs:subClassOf max(?P, ?x))
--           lessThan(?x, ?n)  ->  (?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: (?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) ]
--
--						
--#------------------------------------------------------------------
--# min cardinality
--#------------------------------------------------------------------
--
--[minRec: (?C owl:equivalentClass min(?P, 1)), notEqual(?P, rdf:type) ->
--    [min2b: (?X rdf:type ?C) <- (?X ?P ?Y)] ]
--
--#------------------------------------------------------------------
--# max cardinality 1
--#------------------------------------------------------------------
--
--[maxRec: (?C owl:equivalentClass max(?P, 1)), (?P rdf:type owl:FunctionalProperty)
--		-> (owl:Thing rdfs:subClassOf ?C) ]
--
--#------------------------------------------------------------------
--# 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 owl:equivalentClass ?C)]
--	
--[cardRec1: (?C owl:equivalentClass card(?P, 0)), (?P rdfs:domain ?D), (?E owl:disjointWith ?D)
--	-> (?E owl:equivalentClass ?C)]
--	
--#------------------------------------------------------------------
--# cardinality 1
--#------------------------------------------------------------------
--
--[restriction-inter-CFP: (?C owl:equivalentClass card(?P, 1)), (?P rdf:type owl:FunctionalProperty) ->
--     (?C owl:equivalentClass min(?P, 1)) ]
--
--[restriction6: (?C owl:equivalentClass min(?P, ?X)), (?C owl:equivalentClass max(?P, ?X)) 
--       					-> (?C owl:equivalentClass card(?P, ?X))]
--
--#------------------------------------------------------------------
--# 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)  ] ]
--
--[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) ] ]
--				
--[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)] ]
--
--[validationIndiv3: (?v rb:validation on()) ->
--	[validationIndiv: (?I rb:violation error('conflict', 'Individual a member of Nothing', ?I)) 
--				<- (?I rdf:type owl:Nothing) ] ]
--
--[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 micro rule set v0.1
++# This rule set is designed to implement owl(f)lite using the hybrid
++# rule system (mixture of forward and backward chaining).
++#
++# This differs from the normal OWL rule set in several ways.
++#  - no equality reasoning (sameAs, FunctionalProperty ...)
++#  - omits the someValuesFrom => bNode entailments.
++#  - avoids any guard clauses which would break the find() contract.
++#  - TGC for subClass hierarchies, all subClassOf derivations are forward.
++#  - omits use of prototypes and relies on explicit rules for subClassOf 
++#    derivations this may lead to additional incompletenesses
++#
++# $Id: owl-fb.rules,v 1.45 2004/03/02 13:38:53 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
++#------------------------------------------------------------------
++
++[rdf1and4: (?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)] ] 
++[rdfs5b: (?a rdf:type rdf:Property) -> (?a rdfs:subPropertyOf ?a)] 
++[rdfs6:  (?p rdfs:subPropertyOf ?q), notEqual(?p,?q) -> table(?p, ?q), [ (?a ?q ?b) <- (?a ?p ?b)] ] 
++[rdfs7:  (?a rdf:type rdfs:Class) -> (?a rdfs:subClassOf ?a)]
++[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)]
++
++[rdfs9-alt:  (?a rdf:type ?y) <- bound(?y) (?x rdfs:subClassOf ?y), (?a rdf:type ?x) ] 
++[rdfs9-alt:  (?a rdf:type ?y) <- unbound(?y) (?a rdf:type ?x) (?x rdfs:subClassOf ?y) ] 
++
++#------------------------------------------------------------------
++# 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).
++
++# 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), (owl:Nothing rdfs:subClassOf ?C)]
++
++#------------------------------------------------------------------
++# 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 owl:Class), (?Q rdf:type owl:Class) 
++						-> (?P owl:equivalentClass ?Q) ]
++		
++#------------------------------------------------------------------
++# 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) ]
++
++# SymmetricProperty
++
++[symmetricProperty1: (?P rdf:type owl:SymmetricProperty) -> table(?P),
++                     [symmetricProperty1b: (?X ?P ?Y) <- (?Y ?P ?X)] ]
++
++
++# inverseOf
++[inverseOf1: (?P owl:inverseOf ?Q) -> (?Q owl:inverseOf ?P) ]
++
++[inverseOf2: (?P owl:inverseOf ?Q) -> table(?P), table(?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) -> table(?P),
++#			[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) ]
++						
++#------------------------------------------------------------------
++# 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)).
++
++#------------------------------------------------------------------
++# 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))]
++       					
++[hasValueRec: (?C owl:onProperty ?P), (?C owl:hasValue ?V)
++	-> (?C owl:equivalentClass hasValue(?P, ?V)) ]
++						
++
++## TODO do we need the early restriction propagation rules in this configuration?
++
++# Equality propagation
++
++[restrictionEq1: (?R1 owl:equivalentClass some(?P, ?C)) (?R2 owl:equivalentClass some(?P, ?C))
++					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
++[restrictionEq2: (?R1 owl:equivalentClass all(?P, ?C)) (?R2 owl:equivalentClass all(?P, ?C))
++					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
++[restrictionEq3: (?R1 owl:equivalentClass min(?P, ?C)) (?R2 owl:equivalentClass min(?P, ?C))
++					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
++[restrictionEq4: (?R1 owl:equivalentClass max(?P, ?C)) (?R2 owl:equivalentClass max(?P, ?C))
++					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
++[restrictionEq5: (?R1 owl:equivalentClass card(?P, ?C)) (?R2 owl:equivalentClass card(?P, ?C))
++					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
++[restrictionEq6: (?R1 owl:equivalentClass hasValue(?P, ?C)) (?R2 owl:equivalentClass hasValue(?P, ?C))
++					notEqual(?R1, ?R2) -> (?R1 owl:equivalentClass ?R2) ]
++					
++#[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) ]
++
++
++#------------------------------------------------------------------
++# 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
++
++#------------------------------------------------------------------
++# Intersection of (instance reasoning is done by the translation hook)
++#------------------------------------------------------------------
++
++[intersectionOf1:  (?C owl:intersectionOf ?L) -> listMapAsObject(?C rdfs:subClassOf ?L) ]
++
++#------------------------------------------------------------------
++# someValuesFrom - recognition direction only
++#------------------------------------------------------------------
++    
++[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) ] ]
++
++# In the absence of prototype and bNode introduction rules we have to manually
++# code in additional subclass relationships
++
++[restriction-inter-MnS: (?P rdfs:range ?D), (?C rdfs:subClassOf min(?P, 1)) 
++						-> (?C rdfs:subClassOf some(?P, ?D)) ]
++						
++#------------------------------------------------------------------
++# allValuesFrom (main rule is in Mini, this just does minimal subclass propagation
++#------------------------------------------------------------------
++
++[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)) ]
++    
++[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) ]
++						
++#------------------------------------------------------------------
++# Restricted support for hasValue, even though that is beyond OWL/lite
++#------------------------------------------------------------------
++
++# hasValue
++[hasValueIF: (?C owl:equivalentClass hasValue(?P, ?V)) -> 
++								[ (?x ?P ?V) <- (?x rdf:type ?C) ]
++								[ (?x rdf:type ?C) <- (?x ?P ?V) ]
++								]
++
++#------------------------------------------------------------------
++# Nothing
++#------------------------------------------------------------------
++    
++[nothing1: (?C rdfs:subClassOf min(?P, ?n)) (?C rdfs:subClassOf max(?P, ?x))
++           lessThan(?x, ?n)  ->  (?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: (?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) ]
++
++						
++#------------------------------------------------------------------
++# min cardinality
++#------------------------------------------------------------------
++
++[minRec: (?C owl:equivalentClass min(?P, 1)), notEqual(?P, rdf:type) ->
++    [min2b: (?X rdf:type ?C) <- (?X ?P ?Y)] ]
++
++#------------------------------------------------------------------
++# max cardinality 1
++#------------------------------------------------------------------
++
++[maxRec: (?C owl:equivalentClass max(?P, 1)), (?P rdf:type owl:FunctionalProperty)
++		-> (owl:Thing rdfs:subClassOf ?C) ]
++
++#------------------------------------------------------------------
++# 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 owl:equivalentClass ?C)]
++	
++[cardRec1: (?C owl:equivalentClass card(?P, 0)), (?P rdfs:domain ?D), (?E owl:disjointWith ?D)
++	-> (?E owl:equivalentClass ?C)]
++	
++#------------------------------------------------------------------
++# cardinality 1
++#------------------------------------------------------------------
++
++[restriction-inter-CFP: (?C owl:equivalentClass card(?P, 1)), (?P rdf:type owl:FunctionalProperty) ->
++     (?C owl:equivalentClass min(?P, 1)) ]
++
++[restriction6: (?C owl:equivalentClass min(?P, ?X)), (?C owl:equivalentClass max(?P, ?X)) 
++       					-> (?C owl:equivalentClass card(?P, ?X))]
++
++#------------------------------------------------------------------
++# 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)  ] ]
++
++[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) ] ]
++				
++[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)] ]
++
++[validationIndiv3: (?v rb:validation on()) ->
++	[validationIndiv: (?I rb:violation error('conflict', 'Individual a member of Nothing', ?I)) 
++				<- (?I rdf:type owl:Nothing) ] ]
++
++[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) ] ]
++
++