Re: OWL reasoning in rules

On 29 May 2007, at 15:07, Jeremy Carroll wrote:

>
>
> 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 meant "an ontology that is consistent (i.e., it has models) but  
that has no finite models (i.e., only infinite ones)":

so, here is one (I hope my syntax is ok): zero is an individual,  
Number and Positive are classes, hasSucc and hasPred are properties  
--- and I have chosen these names to help you see the structure of a  
model:

%% zero is a number, but not positive
zero InstanceOf (Number And ComplementOf(Positive))

%% every Number has a positive number as a successor
Number SubClassOf (some hasSucc (Number And Positive))

%% hasPred is the inverse of hasSucc
hasPred (InversePropertyOf hasSucc)

%%
Number SubClassOf (atmost 1 hasPred)

Cheers, Uli


> 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
>
> Jeremy
>
>
>
> -- 
> Hewlett-Packard Limited
> registered Office: Cain Road, Bracknell, Berks RG12 1HN
> Registered No: 690597 England
>

Ulrike Sattler
sattler@cs.man.ac.uk
http://www.cs.man.ac.uk/~sattler/