- From: Jeremy Carroll <jjc@hpl.hp.com>
- Date: Tue, 28 Jan 2003 18:01:29 +0100
- To: www-webont-wg@w3.org
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