W3C home > Mailing lists > Public > www-webont-wg@w3.org > January 2003

RE: question: datatype reasoning?

From: Jeremy Carroll <jjc@hpl.hp.com>
Date: Tue, 28 Jan 2003 18:01:29 +0100
To: www-webont-wg@w3.org
Message-Id: <200301281801.29820.jjc@hpl.hp.com>


Ian

I haven't really grokked your reference:

[1] 
http://www.cs.man.ac.uk/~panz/Zhilin/download/Paper/Pan-Horrocks-datatype-2002.pdf

however, what I understood was the following:

- all datavalues from all datatypes are put into a single set (let's call it 
rdfs:Literal, maybe)

- individual datatypes are represented as unary predicates so that
 xsd:int( "1"^^xsd:decimal ) = true

- two binary predicates equality and inequality are provided over the set of 
all datavalues

- when reasoning about datatypes the algorithm does the usual tableaux 
expansion and tries all possible values (?? much doubt on my part) 
interacting with the datatype oracle using = and !=, and the unary type 
predicates - all with specific arguments.

If this is correct then the algorithm only works for finite datatypes and 
cannot do some DL entailments like:

DatavaluedProperty(p, range(xsd:NMTOKEN) )

DL_entails

DatavaluedProperty(p, range(xsd:string) )

because there are an infinite set of values to test.

Please confirm that I need to read more carefully!

Jeremy
Received on Tuesday, 28 January 2003 12:00:35 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:57 GMT