@prefix dc: <http://purl.org/dc/elements/1.1/> .

<> dc:description """A specification of OWL, in progress""",
 "$Id: ontAx.n3,v 1.9 2003/06/28 12:18:49 jderoo Exp $";
  dc:source <http://www.w3.org/TR/2002/WD-owl-features-20020729/>,
	<http://www.agfa.com/w3c/euler/owl-rules>.

#@prefix ont:  <http://www.w3.org/2001/10/daml+oil#>.
#@prefix ont:  <http://www.w3.org/2002/07/owl#>.
@prefix ont: <http://www.daml.org/2001/03/daml+oil#>.

@prefix l: <http://www.daml.org/2001/03/daml+oil#>. # @@switch to rdf ns

@prefix r: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix s: <http://www.w3.org/2000/01/rdf-schema#> .

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix ontA: <http://www.w3.org/2002/03owlt/ontAx#>.
@prefix : <http://www.w3.org/2002/03owlt/ontAx#>.


this log:forAll :S, :T, :P, :O, :C, :C2, :L, :L2.

# 2.1.1 OWL Lite RDF Schema Features Synopsis
<> s:seeAlso <http://www.w3.org/2000/10/swap/util/rdfs-rules.n3>.

ont:Class s:label "Class";
  s:subClassOf s:Class.


# 2.1.2 OWL Lite Equality and Inequality Synopsis

#hm... these are sorta redundant...
ont:sameClassAs a ont:TransitiveProperty,
  ont:SymmetricProperty.

{ :S ont:sameClassAs :O }
  log:means { :S s:subClassOf :O. :O s:subClassOf :S }.

#hm... these are sorta redundant...
ont:samePropertyAs a ont:TransitiveProperty,
  ont:SymmetricProperty.
{ :S ont:samePropertyAs :O }
  log:means { :S s:subPropertyOf :O. :O s:subPropertyOf :S }.

ont:sameAs a ont:TransitiveProperty,
  ont:SymmetricProperty.
{ :S ont:sameAs :T;
     :P :O }
  log:implies { :T :P :O }.
{ :S :P :O.
  :O ont:sameAs :T }
  log:implies { :S :P :T }.

ont:differentIndividualFrom a ont:SymmetricProperty;
  :_converse ont:sameAs.

# a limited form of negation...
:_converse a ont:SymmetricProperty.
{ { :S [ :_converse :P ] :O } a log:Falsehood } log:implies { :S :P :O }.
{ :S [ :_converse :P ] :O } log:implies { { :S :P :O } a log:Falsehood }.



# 2.1.3 OWL Lite Property Characteristics Synopsis

ont:inverseOf a ont:SymmetricProperty.
{ :S [ ont:inverseOf :P] :O } log:implies { :O :P :S }.

{ :P a ont:TransitiveProperty.
  :S :P [ :P :O ] } log:implies { :S :P :O }.

{ :P a ont:SymmetricProperty.
  :S :P :O } log:implies { :O :P :S }.

{  :P a ont:FunctionalProperty. } log:implies
 { { :S :P :O. :S :P :T. } log:implies  { :O = :T } }.

{  :P a ont:InverseFunctionalProperty. } log:implies
 { { :S :P :O. :T :P :O. } log:implies  { :S = :T } }.

{ :S a [ ont:onProperty :P; ont:allValuesFrom :C ].
  :S :P :O }
  log:implies { :O a :C }.

{ :S a [ ont:onProperty :P; ont:someValuesFrom :C ].}
  log:implies { :S :P [ a :C ] }.


# 2.1.4 OWL Lite Restricted Cardinality Synopsis

# I'm gonna persue a slightly different design here...

{ :C ont:hasAtMostOne :P.
  :S a :C; :P :O, :T.

  :O log:notEqualTo :T. # cwm-specific efficiency hack

 } log:implies { :O = :T }.

<> :note "@@not sure what to do with maxCardinality 0".

# 2.1.5 OWL Lite Datatypes Synopsis

#@@ do datatypes too.


# 2.1.6 OWL Lite Header Information Synopsis

<> :note "@@no axioms from 2.1.6 OWL Lite Header Information Synopsis?".


#####################
# @@@@
# Stuff below here is probably bogus.

# 2.2.1 OWL Class Axioms Synopsis

{ :C ont:oneOf [ ont:item :S] } log:implies { :S a :C }.

# this is sorta redudnant?
{ :C ont:oneOf :L.
  :L l:rest :L2.
  :C2 ont:oneOf :L2 } log:implies { :C2 s:subClassOf :C }.

<> :note "@@hmm... what happened ot ont:item?".

l:first a ont:FunctionalProperty. #@@domain? range?
l:rest a ont:FunctionalProperty.

{ :L l:first :S } log:implies { :L :_item :S }.
{ :L l:rest [ :_item :S ] } log:implies { :L :_item :S }.

<> :note "@@odd form of negation used to say nil has no first/rest".
{ l:nil l:first [] } log:implies { <> a log:Falsehood }.
{ l:nil l:rest [] } log:implies { <> a log:Falsehood }.


<> :note """does owl:Thing include strings, dates, and such?
            or just individuals?""".

# These should be derivable from the axiomatic semantics for DAML+OIL

this log:forAll :x, :y, :z, :p, :q, :C, :C1, :C2, :L.

{ :x = :y } log:implies { :y = :x }. # symmetric
{ :x = [ = :z] } log:implies { :x = :z }. # transitive
{ :x :p :y. :x = :z. :p log:notEqualTo log:forAll, log:forSome} log:implies { :z :p :y }.
{ :x :p :y. :p = :q. :p log:notEqualTo log:forAll, log:forSome} log:implies { :x :q :y }.
{ :x :p :y. :y = :z. :p log:notEqualTo log:forAll, log:forSome} log:implies { :x :p :z }.

{ :x ont:sameAs :y } log:implies { :y ont:sameAs :x }. # symm
{ [ ont:sameAs :x] :p :y } log:implies { :x :p :y }.
{ :x :p [ ont:sameAs :y] } log:implies { :x :p :y }.


{ :p ont:samePropertyAs :q } log:implies { :q ont:samePropertyAs :p }. # symm
{ :x [ ont:samePropertyAs :p] :y } log:implies { :x :p :y }.


{  :p a ont:UnambiguousProperty. } log:implies
 { { :x :p :z. :y :p :z. } log:implies  { :x = :y } }.


#######

{ :x a ont:Nothing } log:implies { :x a :SymptomOfInconsistency }.

{ :C ont:onProperty :p; ont:hasValue :z.
  :x :p :z }
  log:implies { :x a :C}.

{ :x a :C1, :C2.
  :C1 log:notEqualTo :C2. # optimization/hack

  :C ont:intersectionOf (:C1 :C2)
} log:implies { :x a :C }.

{ :x a [ ont:intersectionOf (:C1 :C2) ]
} log:implies { :x a :C1, :C2 }. #@@ and so on, for larger lists



#@@
# commented out due to cwm bug...
#{ :x ont:first :y } log:implies { :x ont:item :y }.
#{ :x ont:rest [ ont:item :y ] } log:implies { :x ont:item :y }.



######
# closed list stuff

{ :x ont:differentIndividualFrom :y. #@@ hack to bind :x
}
  log:implies { :x a ont:Thing }.

{ :x a [ ont:complementOf [ ont:oneOf :L ] ].
  :x ont:differentIndividualFrom :y.

  :C ont:complementOf [ ont:oneOf [ ont:first :y; ont:rest :L ] ].
}
  log:implies { :x a :C }.

ont:Nothing ont:oneOf ().
ont:Thing ont:complementOf ont:Nothing.

# some comprehensions... NOPE.
# the complement of every enumeration exists...
#{ :C ont:oneOf :L } log:implies { [ ont:complementOf :C ] }.
# for every non-empty enumeration, a class one smaller exists...
#{ :C ont:oneOf [ ont:first :x; ont:rest :L ] }
#  log:implies { [ ont:oneOf :L ] }.