#------------------------------------------------------------------
# OWL rule set v0.2
# This rule set is designed to implement owl(f)lite using the hybrid
# rule system (mixture of forward and backward chaining).
#
# Warning: This version is under active development and the moment
# and should NOT be regard as stable or usable.
#
# $Id: owl-fb-old.rules,v 1.2 2004-07-02 08:08:21 der Exp $
#------------------------------------------------------------------

#------------------------------------------------------------------
# RDFS Axioms
#------------------------------------------------------------------

-> (rdf:type      rdfs:range rdfs:Class).
-> (rdfs:Resource  rdf:type  rdfs:Class).
-> (rdfs:Literal   rdf:type  rdfs:Class).
-> (rdf:Statement  rdf:type  rdfs:Class).
-> (rdf:nil        rdf:type  rdf:List).
-> (rdf:subject    rdf:type  rdf:Property).
-> (rdf:object     rdf:type  rdf:Property).
-> (rdf:predicate  rdf:type  rdf:Property).
-> (rdf:first      rdf:type  rdf:Property).
-> (rdf:rest       rdf:type  rdf:Property).
        
-> (rdfs:subPropertyOf rdfs:domain rdf:Property).
-> (rdfs:subClassOf rdfs:domain rdfs:Class).
-> (rdfs:domain rdfs:domain rdf:Property).
-> (rdfs:range rdfs:domain rdf:Property).
-> (rdf:subject rdfs:domain rdf:Statement).
-> (rdf:predicate rdfs:domain rdf:Statement).
-> (rdf:object rdfs:domain rdf:Statement).
-> (rdf:first rdfs:domain rdf:List).
-> (rdf:rest rdfs:domain rdf:List).

-> (rdfs:subPropertyOf rdfs:range rdf:Property).
-> (rdfs:subClassOf rdfs:range rdfs:Class).
-> (rdfs:domain rdfs:range rdfs:Class).
-> (rdfs:range rdfs:range rdfs:Class).
-> (rdf:type rdfs:range rdfs:Class).
-> (rdfs:comment rdfs:range rdfs:Literal).
-> (rdfs:label rdfs:range rdfs:Literal).
-> (rdf:rest rdfs:range rdf:List).

-> (rdf:Alt rdfs:subClassOf rdfs:Container).
-> (rdf:Bag rdfs:subClassOf rdfs:Container).
-> (rdf:Seq rdfs:subClassOf rdfs:Container).
-> (rdfs:ContainerMembershipProperty rdfs:subClassOf rdf:Property).

-> (rdfs:isDefinedBy rdfs:subPropertyOf rdfs:seeAlso).

-> (rdf:XMLLiteral rdf:type rdfs:Datatype).
-> (rdfs:Datatype rdfs:subClassOf rdfs:Class).

#------------------------------------------------------------------
# RDFS Closure rules
#------------------------------------------------------------------

# This one could be omitted since the results are not really very interesting!
#[rdf1and4: (?x ?p ?y) -> (?p rdf:type rdf:Property), (?x rdf:type rdfs:Resource), (?y rdf:type rdfs:Resource)]

[rdfs7b: (?a rdf:type rdfs:Class) -> (?a rdfs:subClassOf rdfs:Resource)] 

[rdfs2:  (?p rdfs:domain ?c) -> [(?x rdf:type ?c) <- (?x ?p ?y)] ] 
[rdfs3:  (?p rdfs:range ?c)  -> [(?y rdf:type ?c) <- (?x ?p ?y), notFunctor(?y)] ] 
[rdfs5a: (?a rdfs:subPropertyOf ?b), (?b rdfs:subPropertyOf ?c) -> (?a rdfs:subPropertyOf ?c)] 
[rdfs5b: (?a rdf:type rdf:Property) -> (?a rdfs:subPropertyOf ?a)] 
[rdfs6:  (?p rdfs:subPropertyOf ?q), notEqual(?p,?q) -> [ (?a ?q ?b) <- (?a ?p ?b)] ] 
[rdfs7:  (?a rdf:type rdfs:Class) -> (?a rdfs:subClassOf ?a)]
[rdfs8:  (?a rdfs:subClassOf ?b), (?b rdfs:subClassOf ?c) -> (?a rdfs:subClassOf ?c)] 
[rdfs9:  (?x rdfs:subClassOf ?y), notEqual(?x,?y) -> [ (?a rdf:type ?y) <- (?a rdf:type ?x)] ] 
[rdfs10: (?x rdf:type rdfs:ContainerMembershipProperty) -> (?x rdfs:subPropertyOf rdfs:member)] 

[rdfs2-partial: (?p rdfs:domain ?c) -> (?c rdf:type rdfs:Class)]
[rdfs3-partial: (?p rdfs:range ?c)  -> (?c rdf:type rdfs:Class)]

#------------------------------------------------------------------
# RDFS iff extensions needed for OWL
#------------------------------------------------------------------

[rdfs2a: (?x rdfs:domain ?y), (?y rdfs:subClassOf ?z) -> (?x rdfs:domain ?z)]
[rdfs3a: (?x rdfs:range  ?y), (?y rdfs:subClassOf ?z) -> (?x rdfs:range  ?z)]

[rdfs12a: (rdf:type rdfs:subPropertyOf ?z), (?z rdfs:domain ?y) -> (rdfs:Resource rdfs:subClassOf ?y)]
[rdfs12a: (rdfs:subClassOf rdfs:subPropertyOf ?z), (?z rdfs:domain ?y) -> (rdfs:Class rdfs:subClassOf ?y)]
[rdfs12a: (rdfs:subPropertyOf rdfs:subPropertyOf ?z), (?z rdfs:domain ?y) -> (rdf:Property rdfs:subClassOf ?y)]

[rdfs12b: (rdfs:subClassOf rdfs:subPropertyOf ?z), (?z rdfs:range ?y) -> (rdfs:Class rdfs:subClassOf ?y)]
[rdfs12b: (rdfs:subPropertyOf rdfs:subPropertyOf ?z), (?z rdfs:range ?y) -> (rdf:Property rdfs:subClassOf ?y)]

#------------------------------------------------------------------
# OWL axioms
#------------------------------------------------------------------

-> (rdf:first rdf:type owl:FunctionalProperty).
-> (rdf:rest rdf:type owl:FunctionalProperty).

-> (rdfs:domain owl:SymmetricProperty owl:ObjectProperty).
-> (rdfs:domain owl:TransitiveProperty owl:ObjectProperty).
-> (rdfs:domain owl:InverseFunctionalProperty owl:ObjectProperty).

-> (rdfs:range owl:ObjectProperty owl:Thing).
-> (rdfs:domain owl:ObjectProperty owl:Thing).
-> (rdfs:domain owl:DatatypeProperty owl:Thing).

-> (owl:Class rdfs:subClassOf rdfs:Class).
-> (owl:Restriction rdfs:subClassOf owl:Class).

# The distinction between rdfs and owl class with disappear. 
# Adding this in introduces rather a lot of duplicate reasoning paths
# which slow things down for no purpose.
#-> (rdfs:Class rdfs:subClassOf owl:Class).

-> (owl:Thing rdf:type owl:Class).

# These might need to be pre-expanded in the initial rule set
-> (owl:equivalentProperty rdf:type owl:SymmetricProperty).
-> (owl:equivalentProperty rdf:type owl:TransitiveProperty).
-> (owl:equivalentClass rdf:type owl:SymmetricProperty).
-> (owl:equivalentClass rdf:type owl:TransitiveProperty).
-> (owl:sameIndividualAs rdf:type owl:SymmetricProperty).
-> (owl:sameIndividualAs rdf:type owl:TransitiveProperty).
-> (owl:sameIndividualAs owl:equivalentProperty owl:sameAs).
-> (owl:differentFrom rdf:type owl:SymmetricProperty).

-> (owl:intersectionOf rdfs:domain owl:Class).

#------------------------------------------------------------------
# OWL Rules
#------------------------------------------------------------------

[thing1: (?C rdf:type owl:Class) -> (?C rdfs:subClassOf owl:Thing)]

#------------------------------------------------------------------
# Identify restriction assertions
#------------------------------------------------------------------

[restriction1: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:someValuesFrom ?D)
						-> (?C owl:equivalentClass some(?P, ?D))]
		
[restriction2: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:allValuesFrom ?D)
						-> (?C owl:equivalentClass all(?P, ?D))]
		
[restriction3: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:minCardinality ?X)
						-> (?C owl:equivalentClass min(?P, ?X))]
		
[restriction4: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:maxCardinality ?X)
						-> (?C owl:equivalentClass max(?P, ?X))]
		
[restriction5: (?C rdf:type owl:Restriction), (?C owl:onProperty ?P), (?C owl:cardinality ?X)
						-> (?C owl:equivalentClass card(?P, ?X)), 
						   (?C rdfs:subClassOf min(?P, ?X)), 
						   (?C rdfs:subClassOf max(?P, ?X)) ]
		
[restriction6: (?C rdfs:subClassOf min(?P, ?X)), (?C rdfs:subClassOf max(?P, ?X)) 
       					-> (?C rdfs:subClassOf card(?P, ?X))]
       					
# Needed for the case where ?R is a restriction literal 
# and so does not appear in the subject position
[restrictionSubclass1: (?D owl:equivalentClass ?R), isFunctor(?R) ->
       [restrictionSubclass1b: (?X rdf:type ?D) <- (?X rdf:type ?R)] ]
       
[restrictionSubclass2: (?D owl:equivalentClass ?R), isFunctor(?R) ->
       [restrictionSubclass2b: (?X rdf:type ?R) <- (?X rdf:type ?D)] ]
       
# Temp trial - might replace above       
#[restrictionSubclass1: (?D owl:equivalentClass ?R), isFunctor(?R) , (?X rdf:type ?R) -> (?X rdf:type ?D)]
#[restrictionSubclass2: (?D owl:equivalentClass ?R), isFunctor(?R) , (?X rdf:type ?D) -> (?X rdf:type ?R)]

#------------------------------------------------------------------
# Interactions between cardinalities and some/all
#------------------------------------------------------------------

[restrictionMS-A: (?C rdfs:subClassOf max(?P, 1)), (?C rdfs:subClassOf some(?P, ?D))
						-> (?C rdfs:subClassOf all(?P, ?D)) ]

[restrictionFS-A: (?P rdf:type owl:FunctionalProperty), (?C rdfs:subClassOf some(?P, ?C))
						 -> (?C rdfs:subClassOf all(?P, ?C)) ]

[restrictionR-S: (?P rdfs:range ?C), notFunctor(?C) ->
     [restrictionRSb: (?X rdf:type some(?P, ?C)) <- (?X ?P ?A) ] ]
     
[restrictionRMn-S: (?P rdfs:range ?D), (?C rdfs:subClassOf min(?P, 1)) 
						-> (?C rdfs:subClassOf some(?P, ?D)) ]

[restrictionRA-T: (?P rdfs:range ?C), (?D owl:equivalentClass all(?P, ?C)) 
						-> (owl:Thing rdfs:subClassOf ?D) ]
						
[restrictionFT-M: (?P rdf:type owl:FunctionalProperty) ->
         [restrictionFTMb: (?X rdf:type max(?P, 1)) <- (?X rdf:type owl:Thing)] ]

# If leave this forward get #ranges * #classes deductions 
# The backward one is only safe if there are no interactions with other forward rules
#[restrictionR-A: (?P rdfs:range ?C), (?D rdf:type owl:Class), notFunctor(?C)  
#						-> (?D rdfs:subClassOf all(?P, ?C)) ]
[restrictionR-A: (?D rdfs:subClassOf all(?P, ?C))
					<- (?P rdfs:range ?C), (?D rdf:type owl:Class), notFunctor(?C) ]
		
[restrictionA-R: (owl:Thing rdfs:subClassOf all(?P, ?C)) 
						-> (?P rdfs:range ?C), (?P rdf:type owl:ObjectProperty) ]

[restriction-S: (?X rdf:type some(?P, ?C)) <- bound(?P), bound(?X), (?X ?P ?V), (?V rdf:type ?C) ]

[restrictionM-N: (?X rdf:type owl:Nothing) <- (?X rdf:type max(?P, 0)), (?X ?P ?A) ]

[restrictionA-Ty: (?C rdfs:subClassOf all(?P, ?D)), notEqual(?P, rdf:type), notEqual(?C, ?D) ->
		[restrictionA-tyb: (?Y rdf:type ?D) <- (?X rdf:type ?C), (?X ?P ?Y) ] ]

# A-Ty + -S implies this so it is redundant (?)
#[restrictionA-S:  (?C rdfs:subClassOf all(?P, ?D)), notEqual(?P, rdf:type) ->
#		[restrictionA-Sb: (?X rdf:type some(?P, ?D)) <- (?X rdf:type ?C), (?X ?P ?Y)] ]

#[restrictionM-sI: (?B owl:sameIndividualAs ?C) <- (?A rdf:type max(?P, 1)), (?A ?P ?B), (?A ?P ?C) ]
[restrictionM-sI: (?C rdfs:subClassOf max(?P, 1)) ->
	[restrictionM-sIb: (?B owl:sameIndividualAs ?C) <- (?A rdf:type ?C), (?A ?P ?B), (?A ?P ?C) ] ]

[restrictionMM-N: (?X rdf:type owl:Nothing) <- (?X rdf:type min(?P, 1)), (?X rdf:type max(?P, 0)) ]

#------------------------------------------------------------------
# Using some(P,C) restriction to infer P values for instances.
# Since this is instance reasoning we should be doing this backwards.
# But we have a problem with makeInstance that we can't create new triples
# during b-rule processing because the deductions graph doesn't support
# concurrent update. We will solve this eventually but for now we revert
# to a forward rule solution.
#------------------------------------------------------------------

#[restrictionS-in: (?C rdfs:subClassOf some(?P, ?D)), notEqual(?P, owl:sameIndividualAs), notEqual(?D, owl:Class), notEqual(?D, rdfs:Class) ->
#           [restrictionS-inb: (?x ?P ?t) <- (?x rdf:type some(?P, ?D)), makeInstance(?x, ?P, ?D, ?t), print('inb', ?x, ?P, ?t) ] 
#           [restrictionS-inb2: (?t rdf:type ?D) <- (?x ?P ?t), noValue(?t, rdf:type), print('inb2', ?t, ?D, ?x) ]
#           ]
           
[restrictionS-in: (?D rdfs:subClassOf some(?P,?C)) (?X rdf:type ?D), noValue(?X, ?P), notEqual(?P, owl:sameIndividualAs),
					notEqual(?C, owl:Class), notEqual(?C, rdfs:Class), 
					notEqual(?P, rdfs:subClassOf), notEqual(?P, rdfs:subPropertyOf), 
					notEqual(?P, owl:equivalentProperty), notEqual(?P, owl:equivalentClass), 
					makeTemp(?T)
   	  						-> (?X ?P ?T), (?T rdf:type ?C)]

#------------------------------------------------------------------
# Create prototypical instances for each class and infer any subclass relations
# This is better done as part of an explicit taxonomy building phase.
# Note that prototype1 requires instance style reasoning so we need derivations
# of type owl:Class to work forwards, hence the special type propagation rules.
#------------------------------------------------------------------

[typeProp1: (?C rdf:type owl:Restriction) -> (?C rdf:type owl:Class) ]
[typeProp2: (?C rdfs:subClassOf ?R), isFunctor(?R) -> (?C rdf:type owl:Class) ]

[prototype1: (?c rdf:type owl:Class), noValue(?c, rb:prototype), makeTemp(?t)
  	    				-> (?c rb:prototype ?t), (?t rdf:type ?c) ]
    
#[prototype1: (?c rdf:type owl:Class), noValue(?c, rb:prototype), makeTemp(?t)
#  	    				-> (?c rb:prototype ?t), (?t rdf:type ?c)
#  	    					 schedulePrototypeCheck(?p, ?c) ]
    
#[prototype2a: (?c rb:prototype ?p), (?c rdfs:subClassOf ?d) (?d rdf:type owl:Restriction)
#					-> schedulePrototypeCheck(?p, ?c) ]
#[prototype2b: (?c rb:prototype ?p), (?c rdf:type owl:Restriction)
#					-> schedulePrototypeCheck(?p, ?c) ]
#[prototype2a: (?c rb:prototype ?p), (?c rdfs:subClassOf ?R) isFunctor(?R)
#					-> schedulePrototypeCheck(?p, ?c) ]

# Back chain version
[prototype2: (?c rb:prototype ?p) ->
                [prototype2b: (?c rdfs:subClassOf ?d) <- (?p rdf:type ?d)] ]
                
[equivalentClass2b: (?P owl:equivalentClass ?Q) 
						<- (?P rdfs:subClassOf ?Q), (?Q rdfs:subClassOf ?P) ]
						
#------------------------------------------------------------------
# Disjointness
#------------------------------------------------------------------

[distinct1: (?C owl:disjointWith ?D), (?X rdf:type ?C), (?Y rdf:type ?D) 
						-> (?X owl:differentFrom ?Y) ]

# Exploding the pairwise assertions is simply done procedurally here.
# This is better handled by a dedicated equality reasoner any.
[distinct2: (?w owl:distinctMembers ?L) -> assertDisjointPairs(?L) ]

# Example version of validation rule, more TBD
[validation1: (?X rdf:type owl:Nothing) <- (?X owl:differentFrom ?Y), (?X owl:sameIndividualAs ?Y)]

#------------------------------------------------------------------
# Class equality
#------------------------------------------------------------------

# equivalentClass
[equivalentClass1: (?P owl:equivalentClass ?Q) 
						-> (?P rdfs:subClassOf ?Q), (?Q rdfs:subClassOf ?P) ]
						
[equivalentClass2: (?P rdfs:subClassOf ?Q), (?Q rdfs:subClassOf ?P) 
						-> (?P owl:equivalentClass ?Q) ]
						
[equivalentClass3: (?P owl:sameAs ?Q), (?P rdf:type rdfs:Class), (?Q rdf:type rdfs:Class) 
						-> (?P owl:equivalentClass ?Q) ]
						
#------------------------------------------------------------------
# Instance equality
#------------------------------------------------------------------

# sameIndividualAs

[sameIndividualAs1: (?P rdf:type owl:FunctionalProperty) ->
      [sameIndividualAs1b: (?B owl:sameIndividualAs ?C) <- unbound(?C), (?A ?P ?B), (?A ?P ?C) ] 
      [sameIndividualAs1b: (?B owl:sameIndividualAs ?C) <-   bound(?C), (?A ?P ?C), (?A ?P ?B) ] 
      ]
                    
[sameIndividualAs2: (?P rdf:type owl:InverseFunctionalProperty) ->
      [sameIndividualAs2b: (?A owl:sameIndividualAs ?C) <- unbound(?C), (?A ?P ?B), (?C ?P ?B) ] 
      [sameIndividualAs2b: (?A owl:sameIndividualAs ?C) <-   bound(?C), (?C ?P ?B), (?A ?P ?B) ] 
      ]
      
# Raw version of above
#[sameIndividualAs1: (?P rdf:type owl:FunctionalProperty) ->
#      [sameIndividualAs1b: (?B owl:sameIndividualAs ?C) <- (?A ?P ?B), (?A ?P ?C) ] ]
#                    
#[sameIndividualAs2: (?P rdf:type owl:InverseFunctionalProperty) ->
#      [sameIndividualAs2b: (?A owl:sameIndividualAs ?C) <- (?A ?P ?B), (?C ?P ?B) ] ]
                    
[sameIndividualAs3: (?X owl:sameAs ?Y), (?X rdf:type owl:Thing), (?Y rdf:type owl:Thing) 
                    -> (?X owl:sameIndividualAs ?Y) ]
                    

[sameIndividualAs4: (?Y ?P ?V) <- unbound(?V), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y), (?X ?P ?V) ]
[sameIndividualAs4: (?Y ?P ?V) <- bound(?V), unbound(?P), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y), (?X ?P ?V) ]
[sameIndividualAs4: (?Y ?P ?V) <- bound(?V), bound(?P), (?X ?P ?V) (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y)  ]
[sameIndividualAs5: (?V ?P ?Y) <- unbound(?V), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y), (?V ?P ?X)  ]
[sameIndividualAs5: (?V ?P ?Y) <- bound(?V), unbound(?P), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y), (?V ?P ?X)  ]
[sameIndividualAs5: (?V ?P ?Y) <- bound(?V), bound(?P), (?V ?P ?X), (?X owl:sameIndividualAs ?Y), notEqual(?X,?Y)  ]

[sameIndividualAs6: (?X rdf:type owl:Thing) <- (?X owl:sameIndividualAs ?Y) ]
[sameIndividualAs6: (?Y rdf:type owl:Thing) <- (?X owl:sameIndividualAs ?Y) ]


#------------------------------------------------------------------
# Property rules
#------------------------------------------------------------------

# equivalentProperty 

[equivalentProperty1: (?P owl:equivalentProperty ?Q) 
						-> (?P rdfs:subPropertyOf ?Q), (?Q rdfs:subPropertyOf ?P) ]
						
[equivalentProperty2: (?P rdfs:subPropertyOf ?Q), (?Q rdfs:subPropertyOf ?P) 
						-> (?P owl:equivalentProperty ?Q) ]
						
[equivalentProperty3: (?P owl:sameAs ?Q), (?P rdf:type rdf:Property), (?Q rdf:type rdf:Property) 
						-> (?P owl:equivalentProperty ?Q) ]

# symmetric
[symmetricProperty1: (?P rdf:type owl:SymmetricProperty) -> 
                     [symmetricProperty1b: (?X ?P ?Y) <- (?Y ?P ?X)] ]


# inverseOf
[inverseOf1: (?P owl:inverseOf ?Q) -> (?Q owl:inverseOf ?P) ]

[inverseOf2: (?P owl:inverseOf ?Q) -> [inversOf2b: (?X ?P ?Y) <- (?Y ?Q ?X)] ]

[inverseOf3: (?P owl:inverseOf ?Q), (?P rdf:type owl:FunctionalProperty) 
						-> (?Q rdf:type owl:InverseFunctionalProperty) ]
		
[inverseOf4: (?P owl:inverseOf ?Q), (?P rdf:type owl:InverseFunctionalProperty) 
						-> (?Q rdf:type owl:FunctionalProperty) ]

# Transitive
[transitiveProperty1: (?P rdf:type owl:TransitiveProperty) ->
			[transitiveProperty1b:  (?A ?P ?C) <- (?A ?P ?B), (?B ?P ?C)] ]


#------------------------------------------------------------------
# if-only parts of additional constructs
#------------------------------------------------------------------

# hasValue
[hasValue1: (?c rdf:type owl:Restriction), (?c owl:onProperty ?p), (?c owl:hasValue ?v) ->
		[hasValue1b: (?x ?p ?v) <- (?x rdf:type ?c) ] ]

#------------------------------------------------------------------
# Unused rules - attempted tuning but builtin clause reordering does well enough
#------------------------------------------------------------------

#[transitiveProperty1: (?P rdf:type owl:TransitiveProperty) ->
#			[transitiveProperty1b:  (?A ?P ?C) <- unbound(?C), (?A ?P ?B), (?B ?P ?C)] 
#			[transitiveProperty1b:  (?A ?P ?C) <-   bound(?C), (?B ?P ?C), (?A ?P ?B)] 
#			]