# $Id: russel-dpo.n3,v 1.5 2004/06/25 01:26:59 timbl Exp $
#
# taken from
#  A Proposal for the Web Ontology Language - slide "DAML+OIL Paradox"
#  http://www-db.research.bell-labs.com/user/pfps/talks/webont-f2f-owl/slide25-0.html
#
# see also, discussion with bijan in #rdfig
# http://ilrt.org/discovery/chatlogs/rdfig/2002-01-17#T22-14-42

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

@prefix list: <cwm-lists-are-broken#>.
@prefix form: <cwm-formula-printing-is-broken#>.

@prefix : <#>.

@forSome :_g1 .

:_g1 a :_g1, owl:Restriction;
 owl:hasClassQ [ owl:oneOf [ list:first :_g1; list:rest list:nil] ];
   owl:maxCardinalityQ "0";
   owl:onProperty rdf:type .


#####
# background... some rules/axioms to define the DAML+OIL/owl terms...

@forAll :s, :p, :o, :C, :C1, :C2, :F,
	:sn, :pn, :on.


# some axioms about oneOf...
# oneOf relates a class to a list of its members.
# { x, y, z } is basically written [ owl:oneOf ( :x :y :z ) ].

# First, the axiom of singletons:
# for all :s, :s a { :s }.
{ [ list:first :s ]. } # cwm needs something to trigger from...
 log:implies { :s a [ owl:oneOf [ list:first :s; list:rest list:nil] ]. }.

# next, since we don't have function symbols,
# we need to say that any member of {x} is a member of {x}.
{ :C1 owl:oneOf [ list:first :o; list:rest list:nil ].
  :C2 owl:oneOf [ list:first :o; list:rest list:nil ].
  :s a :C1 }
  log:implies { :s a :C2 }.

# now an axiom obout hasClassQ...
#
# In general,
# [ owl:hasClassQ :C; owl:maxCardinalityQ N;    owl:onProperty :p ]
#  is the/a class of things with at most N different values
#  from class :C
#  of the property :p.
# a (not so good) example: every person has at most 2 parents that are Persons:
#  :Person rdfs:subClassOf [
#    owl:onProperty :parent;
#    owl:maxCardinalityQ "2";
#    owl:hasClassQ :Person].
#
# hence if N is zero and :o is a :C,
# then :s is not related to :o by :p.
#
{ :s a [ owl:hasClassQ :C; owl:maxCardinalityQ "0";    owl:onProperty :p ].
  :o a :C.

  :s log:uri :sn.
  :p log:uri :pn.
  :o log:uri :on.

 }
  log:implies {
   # I tried writing
   #   { :s :p :o } a log:Falsehood.
   # but cwm seems to have trouble with {}s nested in the conclusion, so
   # I'm making up this funky form of reification...
   [ form:subject :sn; form:predicate :pn; form:object :on ]
    a log:Falsehood
  }.


# Finally
# if P and not(P), then P is Goofy!
{ :s :p :o.
  :F form:subject [ is log:uri of :s];
     form:predicate [ is log:uri of :p];
     form:object [is log:uri of :o].
  :F a log:Falsehood }
  log:implies {
   :F a :Goofy. }.