# Copyright World Wide Web Consortium, (Massachusetts Institute of
# Technology, Institut National de Recherche en Informatique et en
# Automatique, Keio University).
#
# All Rights Reserved.
#
# Please see the full Copyright clause at
# <http://www.w3.org/Consortium/Legal/copyright-software.html>
#
# $Id: axioms.n3,v 1.5 2001/10/17 08:19:18 josderoo Exp $
##################################################################

@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix mt: <http://www.w3.org/TR/rdf-mt/#> .
@prefix : <axioms#> .

rdf:type rdf:type rdf:Property .
rdfs:Resource rdf:type rdfs:Class .
rdfs:Literal rdf:type rdfs:Class .
rdfs:Class rdf:type rdfs:Class .
rdf:Property rdf:type rdfs:Class .
rdf:type rdf:type rdf:Property .
rdf:type rdfs:domain rdfs:Resource .
rdf:type rdfs:range rdfs:Class .
rdfs:domain rdf:type rdf:Property .
rdfs:domain rdfs:domain rdf:Property .
rdfs:domain rdfs:range rdfs:Class .
rdfs:range rdf:type rdf:Property .
rdfs:range rdfs:domain rdf:Property .
rdfs:range rdfs:range rdfs:Class .
rdfs:subPropertyOf rdf:type rdf:Property .
rdfs:subPropertyOf rdfs:domain rdf:Property .
rdfs:subPropertyOf rdfs:range rdf:Property .
rdfs:subClassOf rdf:type rdf:Property .
rdfs:subClassOf rdfs:domain rdfs:Class .
rdfs:subClassOf rdfs:range rdfs:Class .

:RDF-RULE-1 rdfs:isDefinedBy mt:rdfsentail .
: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 .

{ :RDF-RULE-1 rdfs:isDefinedBy mt:rdfsentail . :s :p :o } log:implies { :p rdf:type rdf:Property } .
{ :RDFS-RULE-2 rdfs:isDefinedBy mt:rdfsentail . :s :p :o . :p rdfs:domain :C } log:implies { :s rdf:type :C } .
{ :RDFS-RULE-3 rdfs:isDefinedBy mt:rdfsentail . :s :p :o . :p rdfs:range :C } log:implies { :o rdf:type :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-5 rdfs:isDefinedBy mt:rdfsentail . :a rdfs:subPropertyOf :b. :b rdfs:subPropertyOf :c } log:implies { :a rdfs:subPropertyOf :c } .
{ :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-8 rdfs:isDefinedBy mt:rdfsentail . :A rdfs:subClassOf :B. :B rdfs:subClassOf :C } log:implies { :A rdfs:subClassOf :C } .
{ :RDFS-RULE-9 rdfs:isDefinedBy mt:rdfsentail . :A rdfs:subClassOf :B. :a a :A } log:implies { :a a :B } .