# $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: .
@prefix log: .
@prefix rdf: .
@prefix list: .
@prefix form: .
@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. }.