# $Id: rdfs-rules.n3,v 1.6 2001/12/01 01:21:28 amdus Exp $

# rules for RDFS entailment

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix ont: <http://www.daml.org/2001/03/daml+oil#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix mt: <http://www.w3.org/TR/rdf-mt/#> .
@prefix : <rdfs-rules#> .

rdfs:Resource a rdfs:Class .
rdfs:Literal a rdfs:Class .
rdfs:Class a rdfs:Class .
rdf:Property a rdfs:Class .

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

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

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

rdfs:subPropertyOf a rdf:Property .
rdfs:subPropertyOf rdfs:domain rdf:Property .
rdfs:subPropertyOf rdfs:range rdf:Property .

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

rdfs:subPropertyOf a ont:TransitiveProperty .
rdfs:subClassOf a ont:TransitiveProperty .

:RDFS-RULE-2 rdfs:isDefinedBy mt:rdfsentail .
:RDFS-RULE-3 rdfs:isDefinedBy mt:rdfsentail .
:RDFS-RULE-4a rdfs:isDefinedBy mt:rdfsentail .
:RDFS-RULE-4b rdfs:isDefinedBy mt:rdfsentail .
:RDFS-RULE-5 rdfs:isDefinedBy mt:rdfsentail .
:RDFS-RULE-6 rdfs:isDefinedBy mt:rdfsentail .
:RDFS-RULE-7 rdfs:isDefinedBy mt:rdfsentail .
:RDFS-RULE-8 rdfs:isDefinedBy mt:rdfsentail .
:RDFS-RULE-9 rdfs:isDefinedBy mt:rdfsentail .

this log:forAll :s, :p, :o, :a, :b, :c, :A, :B, :C .
{ :RDFS-RULE-2 rdfs:isDefinedBy mt:rdfsentail . :s :p :o . :p rdfs:domain :C } log:implies { :s a :C } .
{ :RDFS-RULE-3 rdfs:isDefinedBy mt:rdfsentail . :s :p :o . :p rdfs:range :C } log:implies { :o a :C } .
{ :RDFS-RULE-4a rdfs:isDefinedBy mt:rdfsentail . :s :p :o } log:implies { :s a rdfs:Resource } .
{ :RDFS-RULE-4b rdfs:isDefinedBy mt:rdfsentail . :s :p :o } log:implies { :o a rdfs:Resource } .
{ :RDFS-RULE-6 rdfs:isDefinedBy mt:rdfsentail . :p rdfs:subPropertyOf :b. :s :p :o } log:implies { :s :b :o } .
{ :RDFS-RULE-7 rdfs:isDefinedBy mt:rdfsentail . :C a rdfs:Class } log:implies { :C rdfs:subClassOf rdfs:Resource } .
{ :RDFS-RULE-9 rdfs:isDefinedBy mt:rdfsentail . :A rdfs:subClassOf :B. :a a :A } log:implies { :a a :B } .