W3C home > Mailing lists > Public > semantic-web@w3.org > May 2007

Re: OWL reasoning in rules

From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
Date: Tue, 29 May 2007 10:34:35 -0400 (EDT)
Message-Id: <20070529.103435.45996988.pfps@research.bell-labs.com>
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

	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

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.

Received on Tuesday, 29 May 2007 14:36:18 UTC

This archive was generated by hypermail 2.4.0 : Tuesday, 5 July 2022 08:45:00 UTC