RE: question: datatype reasoning?


I haven't really grokked your reference:


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) )


DatavaluedProperty(p, range(xsd:string) )

because there are an infinite set of values to test.

Please confirm that I need to read more carefully!


Received on Tuesday, 28 January 2003 12:00:35 UTC