- From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
- Date: Tue, 29 May 2007 10:34:35 -0400 (EDT)
- To: jjc@hpl.hp.com
- Cc: sattler@cs.man.ac.uk, matthew.williams@cancer.org.uk, horrocks@cs.man.ac.uk, public-owl-dev@w3.org, semantic-web@w3.org, bparsia@cs.man.ac.uk
From: Jeremy Carroll <jjc@hpl.hp.com> Subject: Re: OWL reasoning in rules Date: Tue, 29 May 2007 15:07:48 +0100 > > > > Ulrike Sattler wrote: > > It is not too difficult to see that we can construct an OWL ontology all > > of whose models are infinite (let me know if you want to see an example > > of such an ontology), e.g., where each model contains an infinite chain > > of fathers *in addition to the fathers that are explicitly present in > > the ontology, > > > Hmmm, I would like to see a small ontology which is necessarily infinite. > > I've just being looking with google, and found my own > http://www.w3.org/TR/owl-test/dl-900-arith#description-logic-908 > > which I believe hinges on > 2*3*n = 5*n & n>0 > implies n >= aleph0, > but I am still trying to understand it. > > thanks for a pointer > There are lots of other ways of requiring an infinite model. One of the simplest, using father but not exactly true-to-life: father <= Human x Human father is a relationship between humans Human <= ( =1 father) ^ ( <=1 father- ) All humans have exactly one father and at most one inverse of father. From this we get that every human has either an infinite chain of fathers or is in a completely isolated cycle of fathers. Otherwise there would be a human with more than one father inverse. John in Human ^ ( <=0 father- ) John is a human with no father inverse. From this John must be the root of an infinite chain of fathers. peter
Received on Tuesday, 29 May 2007 14:36:18 UTC