RE: question: datatype reasoning?

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 UTC