# Meta rules for inference with Notation 3

# Incorporates the rules of Jos De Roo: http://www.agfa.com/w3c/euler/rdfs-rules.n3,
# http://www.agfa.com/w3c/euler/owl-rules.n3 and http://www.agfa.com/w3c/euler/rdfd-theory.n3.

# There are three categories of rules:
# 1) Rules that serve to detect inconsistencies. 
# 2) Rules that are used for typing and generally preparing the db.
#    These always belong also to category 1.
# 3) Rules that are used during the resolution process.

# A rule may belong to more than one type. 
# Before a rule a possible way of implementing is indicated. 

# Problems: a rule can change the cardinality of a fact.
# A rule can change a restriction? 

# Prefix definitions:
 
 @prefix log: <http://www.w3.org/2000/10/swap/log# .
 @prefix math: <http://www.w3.org/2000/10/swap/math# . 
 @prefix owl: <http://www.w3.org/2002/07/owl# . 
 @prefix xsd: <http://www.w3.org/2001/XMLSchema# .
 @prefix rdfs: <http://www.w3.org/2000/01/rdf-schema# . 
 @prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns# . 
 @prefix mt: <http://www.w3.org/TR/rdf-mt/# . 

# I = if something is a functional property mark it as being a class.
# This way it will only unify with something that is a class. 
owl:FunctionalProperty a rdfs:Class . 

owl:InverseFunctionalProperty a rdfs:Class . 

owl:Ontology a rdfs:Class . 

owl:Restriction a rdfs:Class . 

owl:SymmetricProperty a rdfs:Class .

owl:TransitiveProperty a rdfs:Class . 

owl:allValuesFrom a rdf:Property; rdfs:domain owl:Restriction; rdfs:range rdfs:Class .

owl:cardinality a rdf:Property; rdfs:domain owl:Restriction; rdfs:range xsd:nonNegativeInteger . 

owl:complementOf a rdf:Property; a owl:SymmetricProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class .

 owl:differentFrom a rdf:Property; a owl:SymmetricProperty .

owl:disjointWith a rdf:Property; a owl:SymmetricProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . 

owl:equivalentTo a rdf:Property; a owl:SymmetricProperty; a owl:TransitiveProperty .

owl:extension a rdf:Property; rdfs:domain rdf:Property; rdfs:range rdf:List .

owl:hasValue a rdf:Property; rdfs:domain owl:Restriction . 

owl:imports a rdf:Property; rdfs:subPropertyOf rdfs:seeAlso . 

owl:intersectionOf a rdf:Property; rdfs:domain rdfs:Class; rdfs:range rdf:List . 

owl:inverseOf a rdf:Property; a owl:SymmetricProperty . 

owl:item a rdf:Property; rdfs:domain rdf:List . 

owl:maxCardinality a rdf:Property; rdfs:domain owl:Restriction; rdfs:range xsd:nonNegativeInteger . 

owl:minCardinality a rdf:Property; rdfs:domain owl:Restriction; rdfs:range xsd:nonNegativeInteger .

owl:oneOf a rdf:Property; rdfs:domain rdfs:Class; rdfs:range rdf:List .

owl:onProperty a rdf:Property; rdfs:domain owl:Restriction; rdfs:range rdf:Property .

owl:sameClassAs a rdf:Property; a owl:SymmetricProperty; a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class; rdfs:subPropertyOf rdfs:subClassOf .

owl:samePropertyAs a rdf:Property; a owl:SymmetricProperty; a owl:TransitiveProperty; rdfs:subPropertyOf rdfs:subPropertyOf . 

owl:someValuesFrom a rdf:Property; rdfs:domain owl:Restriction; rdfs:range rdfs:Class . owl:unionOf a rdf:Property; rdfs:domain rdfs:Class; rdfs:range rdf:List . 

owl:versionInfo a rdf:Property; rdfs:subPropertyOf rdfs:comment .

### inference rules for Ontology Web Language
# general idea is to put rules to be used during execution in a dictionary and
# mark the name of the rule in the database so it can be used quickly.
# The rule will not be used otherwise??

# I = use during execution;mark instance as owl:inverseOf. T = 3
{:execution :name owl:inverseOf. ?p owl:inverseOf ?q . ?s ?p ?o } log:implies { ?o ?q ?s } . 

# I = use during execution; mark instance as owl:SymmetricProperty. T = 3
{:execution :name owl:SymmetricProperty. ?p a owl:SymmetricProperty . ?s ?p ?o } log:implies { ?o ?p ?s } .

# I = use during execution; mark instance as owl:TransitiveProperty. T = 3.
{:execution :name owl:TransitiveProperty.?p a owl:TransitiveProperty . ?x ?p ?o . ?s ?p ?x } log:implies { ?s ?p ?o } . 

{?p owl:extension ?L . ?L owl:item ( ?s ?o ) } log:implies { ?s ?p ?o } . 

{?a owl:extension ?x . ?b owl:extension ?y . ?x :includes ?y . ?y :includes ?x } log:implies { ?a owl:samePropertyAs ?b } .

# how to implement sets? if stated ?y owl:complementOf ?z  then whenever 
# an element of class ?y is encountered it must be checked whether this
# is not an element of ?z. This can only be enforced in a closed world.
# In the engine each time an element of ?y is matched with an element
# ?q it must be checked wheter not ?q a ?z. Thus an instance of a class
# refers to a class-description where properties like owl:complementOf
# are marked.Thus somewhere a need is for: a class-description and the
# hierarchy of the classes. Put in XML-tree. This means a supplementary
# datastructure for classes, properties etc....
# How to make a class-hierarchy (or property hierarchy? ) 
# use a set of class determining rules and for each defined class ?x
# ask the query: ?what a ?x.
# Besides that a list of elements of classes has to be maintained?

# I = mark in class-description owl:complementOf.
{?y owl:complementOf ?z . ?x owl:complementOf ?y } log:implies { ?x owl:sameClassAs ?z } .

{?a owl:intersectionOf ?x . ?b owl:intersectionOf ?y . ?x :includes ?y . ?y :includes ?x } log:implies { ?a owl:sameClassAs ?b } . 

{?a owl:unionOf ?x . ?b owl:unionOf ?y . ?x :includes ?y . ?y :includes ?x } log:implies { ?a owl:sameClassAs ?b } . 

{?a owl:oneOf ?x . ?b owl:oneOf ?y . ?x :includes ?y . ?y :includes ?x } log:implies { ?a owl:sameClassAs ?b } .

{?x owl:equivalentTo ?z . ?x ?p ?y } log:implies { ?z ?p ?y } . 

{?p owl:equivalentTo ?q . ?x ?p ?y } log:implies { ?x ?q ?y } .

{?y owl:equivalentTo ?z . ?x ?p ?y } log:implies { ?x ?p ?z } .

{?p a owl:FunctionalProperty . ?s ?p ?x . ?s ?p ?y } log:implies { ?x owl:equivalentTo ?y } . 

{?p a owl:InverseFunctionalProperty . ?x ?p ?o . ?y ?p ?o } log:implies { ?x owl:equivalentTo ?y } . 

{?a owl:extension ?x . ?b owl:extension ?y . ?y :includes ?x } log:implies { ?a rdfs:subPropertyOf ?b } .

{?C owl:oneOf ?L . ?L owl:item ?x } log:implies { ?x a ?C } .

{?D owl:intersectionOf ?L . ?L owl:item ?C . ?x a ?D } log:implies { ?x a ?C } . 

{?C owl:intersectionOf ?L . ?x :inAllOf ?L } log:implies { ?x a ?C } .

{?C owl:unionOf ?L . ?x :inSomeOf ?L } log:implies { ?x a ?C } . 

{?a owl:intersectionOf ?x . ?b owl:intersectionOf ?y . ?x :includes ?y } log:implies { ?a rdfs:subClassOf ?b } . 

{?a owl:unionOf ?x . ?b owl:unionOf ?y . ?y :includes ?x } log:implies { ?a rdfs:subClassOf ?b } .

{?a owl:oneOf ?x . ?b owl:oneOf ?y . ?y :includes ?x } log:implies { ?a rdfs:subClassOf ?b } . 

{?a owl:intersectionOf ?x . ?x owl:item ?b } log:implies { ?a rdfs:subClassOf ?b } . 

{?b owl:unionOf ?y . ?y owl:item ?a } log:implies { ?a rdfs:subClassOf ?b } . 

owl:onProperty ?p; owl:allValuesFrom ?C ] ) . ?s ?p ?o } log:implies { ?o a ?C } .

{?s a owl:Object . ?p a owl:FunctionalProperty } log:implies { ?s a ( [ a owl:Restriction; owl:maxCardinality "1"; owl:onProperty ?p ] ) } . 

{?s a owl:Object . ?s a ( [ a owl:Restriction; owl:onProperty ?p; owl:minCardinality ?min ] ) . 

{ ?s ?p ?o } math:proofCount ?n . ?n math:lessThan ?min } log:implies { ?s :inconsistentWith owl:Restriction } . 

{?s a owl:Object . ?s a ( [ a owl:Restriction; owl:onProperty ?p; owl:maxCardinality ?max ] ) . 

{ ?s ?p ?o } math:proofCount ?n . ?max math:lessThan ?n } log:implies { ?s :inconsistentWith owl:Restriction } . 

{ ?x a ?y . ?x a ?z . ?y owl:complementOf ?z } log:implies { ?x :inconsistentWith owl:complementOf } . 

{ ?x owl:complementOf ?y . ?y owl:sameClassAs ?x } log:implies { ?x :inconsistentWith owl:sameClassAs } .

 { ?x a ?y . ?x a ?z . ?y owl:disjointWith ?z } log:implies { ?x :inconsistentWith owl:disjointWith } .

 { ?p a owl:FunctionalProperty . ?s ?p ?x . ?s ?p ?y . ?x owl:differentFrom ?y } log:implies { ?x :inconsistentWith owl:FunctionalProperty } . 

{  ?p a owl:InverseFunctionalProperty . ?x ?p ?o . ?y ?p ?o . ?x owl:differentFrom ?y } log:implies { ?x :inconsistentWith owl:InverseFunctionalProperty } . 

{ ?C owl:oneOf ?L . ?x a ?C . ?L owl:notItem ?x } log:implies { ?x :inconsistentWith owl:oneOf } . 

{ ?p owl:extension ?L . ?s ?p ?o . ?L owl:notItem ( ?s ?o ) } log:implies { ( ?s ?o ) :inconsistentWith owl:extension } . 

# $Id: rdfd-theory.n3,v 1.16 2002/02/11 00:20:21 amdus Exp $ # PxButton | commit | cvs commit -m "prepare for skolem" rdfd-theory.n3 | # axioms for RDFD entailment.

@prefix : <rdfd-theory# .

rdfs:Datatype a rdfs:Class . 

rdf:value a rdf:Property .

rdf:value rdfs:domain rdfs:Resource .

rdf:value rdfs:range rdfs:Literal .

rdf:dtype a rdf:Property .

rdf:dtype rdfs:domain rdfs:Resource .

rdf:dtype rdfs:range rdfs:Datatype .

rdf:dtype rdfs:subPropertyOf rdf:type . 

{ ?d a rdfs:Datatype } log:implies { ?d rdfs:domain ?d } .

{ ?d a rdfs:Datatype . ?s ?d ?o } log:implies { ?s rdf:value ?o } .

{ ?d a rdfs:Datatype . ?p rdfs:range ?d . ?s ?p ?o } log:implies { ?o rdf:dtype ?d } . 

<#rcsid "$Id: rdfs-rules.n3,v 1.22 2002/08/12 10:01:55 amdus Exp $" . ### rules for RDFS entailment  . 

@prefix : <rdfs-rules# . 

rdfs:Class a rdfs:Class . 

rdf:List a rdfs:Class .

rdfs:Literal a rdfs:Class . 

rdf:Property a rdfs:Class .

rdfs:Resource a rdfs:Class . 

rdfs:domain a rdf:Property; rdfs:domain rdf:Property; rdfs:range rdfs:Class . 

rdf:first a rdf:Property; rdfs:domain rdf:List .

rdf:nil a rdf:List . 

rdfs:range a rdf:Property; rdfs:domain rdf:Property; rdfs:range rdfs:Class .

rdf:rest a rdf:Property; rdfs:domain rdf:List; rdfs:range rdf:List . 
rdfs:subClassOf a rdf:Property; rdfs:domain rdfs:Class; rdfs:range 
rdfs:Class . rdfs:subPropertyOf a rdf:Property; rdfs:domain rdf:Property; rdfs:range rdf:Property . 

rdf:type a rdf:Property; rdfs:domain rdfs:Resource; rdfs:range rdfs:Class .

this log:forAll :s, :o, :x, :p, :q, :r, :A, :B, :C . 

# I = mark type property for all properties.
{:s :p :o } log:implies { :p a rdf:Property } . 

{:p rdfs:domain :C . :s :p :o } log:implies { :s a :C } . 

{:p rdfs:range :C . :s :p :o } log:implies { :o a :C } .

{:s :p :o } log:implies { :s a rdfs:Resource } .

{:s :p :o } log:implies { :o a rdfs:Resource } .

{:q rdfs:subPropertyOf :r . :p rdfs:subPropertyOf :q } log:implies { :p rdfs:subPropertyOf :r } . 

{ :p rdfs:subPropertyOf :r . :s :p :o } log:implies { :s :r :o } .

{ ( :p :q ) rdfs:subPropertyOf :r . :x :q :o . :s :p :x } log:implies { :s :r :o } .

{ :C a rdfs:Class } log:implies { :C rdfs:subClassOf rdfs:Resource } . 

{  :B rdfs:subClassOf :C . :A rdfs:subClassOf :B } log:implies { :A rdfs:subClassOf :C } . 

{ :A rdfs:subClassOf :B . :s a :A } log:implies { :s a :B } .