# Schema parsing deeley in Notation3
# Version 0.1 - 21 April 2001

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

<> log:forAll :x1 , :y1 , :x2 , :y2 , :x3 , :y3 , :x4 , :y4 , :x5 , :y5 , 
:x6 , :x7 , :y7 , :z7 , :x8 , :y8 , :z8 , :x9 , :x10 , :x11 , :x12 , :x13 , 
:x14 , :y14 , :x15 , :y15 .

# :x1 , :y1 , 
{ :x1 a rdfs:Class; rdfs:domain :y1 }
log:implies
{ :x1 :schemaInconsistency "Classes cannot have domains" } .

# :x2 , :y2 , 
{ :x2 a rdfs:Class; rdfs:range :y2 }
log:implies
{ :x2 :schemaInconsistency "Classes cannot have ranges" } .

# Axiom:-
rdfs:subClassOf rdfs:range rdfs:Class; rdfs:Domain rdfs:Class .

# :x3 , :y3 , 
# Rule:-
{ :x3 a rdfs:Property; rdfs:subClassOf :y3 }
log:implies
{ :x3 :schemaInconsistency "A property is not a class - cannot be a subClass" } .

# Axiom:-
rdf:type rdfs:range rdfs:Class .

# Rule:-
# :x4 , :y4 , 
{ :x4 rdf:type :y4 . :y4 a rdf:Property . }
log:implies
{ :x4 :schemaInconsistency "Cannot be a type of property, must be class" } .

# Axiom:-
rdf:range rdfs:range rdfs:Class; rdfs:domain rdf:Property .

# Rule:-
# :x5 , :y5 , 
{ :x5 rdfs:range :y5; a rdfs:Class }
log:implies
{ :x5 :schemaInconsistency "Something with a range must be a property" } .

# :x6 ,
{ :x6 a rdf:Property; a rdfs:Class }
log:implies
{ :x6 :schemaInconsistency "A Property cannot be a Class" } .

# :x7 , :y7 , :z7 , 
{ :x7 a rdfs:Class . :y7 :x7 :z7 }
log:implies
{ :x7 :schemaInconsistency "A rdfs:Class cannot be used as a rdf:Property" } .

# :x8 , :y8 , :z8 , 
# { :x8 a rdfs:Literal . :x8 :y8 :z8 }
# log:implies
# { :x8 :schemaInconsistency "A rdfs:Literal cannot be used as a rdf:Subject" } .

# :x9 , 
{ :x9 a rdf:Class }
log:implies
{ :x9 :schemaInconsistency "No such thing as rdf:Class, try rdfs:Class" } .

# :x10 , 
{ :x10 a rdfs:Property }
log:implies
{ :x10 :schemaInconsistency "No such thing as rdfs:Property, try rdf:Property" } .

# :x11 , 
{ :x11 rdfs:type :y11 }
log:implies
{ :x11 :schemaInconsistency "No such thing as rdfs:type, try rdf:type" } .

{ { :x a rdf:Resource }
  log:implies
  { :x :schemaInconsistency 
          """No such thing as rdf:Resource, try rdfs:Resource""" } } 
log:forAll :x .

# :x12 , 
{ :x12 rdf:range :y12 }
log:implies
{ :x12 :schemaInconsistency "No such thing as rdf:range, try rdfs:range" } .

# :x13 , 
{ :x13 rdf:domain :y13 }
log:implies
{ :x13 :schemaInconsistency "No such thing as rdf:domain, try rdfs:domain" } .

# :x14 , :y14 , 
{ :x14 rdf:subClassOf :y14 }
log:implies
{ :x14 :schemaInconsistency "No such thing as rdf:subClassOf, try rdfs:SubClassOf" } .

# :x15 , :y15 , 
{ :x15 rdfs:subClassof :y15 . :y15 rdfs:subClassOf :x15 }
log:implies
{ :x15 :schemaInconsistency """x cannot be a subClass of y when 
y is a subClass of x""" } .

# { rdf:type a rdfs:Class }
# log:implies
# { rdf:type :schemaInconsistency "rdf:type is a Property, not a Class" } .

# { rdfs:label a rdfs:Class }
# log:implies
# { rdfs:label :schemaInconsistency "rdfs:label is a Property, not a Class" } .

# { rdfs:comment a rdfs:Class }
# log:implies
# { rdfs:comment :schemaInconsistency "rdfs:comment is a Property, not a Class" } .

# { rdfs:isDefinedBy a rdfs:Class }
# log:implies
# { rdfs:isDefinedBy :schemaInconsistency "rdfs:isDefinedBy is a Property, not a Class" } .

# { rdfs:seeAlso a rdfs:Class }
# log:implies
# { rdfs:seeAlso :schemaInconsistency "rdfs:seeAlso is a Property, not a Class" } .

# { rdfs:subClassOf a rdfs:Class }
# log:implies
# { rdfs:subClassOf :schemaInconsistency "rdfs:subClassOf is a Property, not a Class" } .

# { rdfs:subPropertyOf a rdfs:Class }
# log:implies
# { rdfs:subPropertyOf :schemaInconsistency "rdfs:subPropertyOf is a Property, not a Class" } .

# { rdfs:range a rdfs:Class }
# log:implies
# { rdfs:range :schemaInconsistency "rdfs:range is a Property, not a Class" } .

# { rdfs:domain a rdfs:Class }
# log:implies
# { rdfs:domain :schemaInconsistency "rdfs:domain is a Property, not a Class" } .

{ :p1 = :p1 } log:implies { :p1 rdfs:comment "contains equivalences" } .

{ {   :x a :y .
      :x a :z .
      :y daml:disjointFrom :z } log:implies 
  { :x a :schemaInconsistency; 
         rdfs:comment "mess up with disjoint somewhere" } 
} log:forAll :x , :y , :z .