From: Ian Horrocks <horrocks@cs.man.ac.uk>

Date: Wed, 29 Jan 2003 22:37:39 +0000

Message-ID: <15928.22451.61188.248724@merlin.horrocks.net>

To: Jeremy Carroll <jjc@hpl.hp.com>

Cc: www-webont-wg@w3.org

Date: Wed, 29 Jan 2003 22:37:39 +0000

Message-ID: <15928.22451.61188.248724@merlin.horrocks.net>

To: Jeremy Carroll <jjc@hpl.hp.com>

Cc: www-webont-wg@w3.org

On January 28, Jeremy Carroll writes: > > > 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. No. The algorithm does the usual tableaux expansion. For each abstract node with datatype successors, there will be a set of constraints on those successors of the kind P(x1,...,xn), NOT P(y1,...,ym), xi!=yj etc. The oracle must answer yes if there exists a set of values that satisfy all the constraints, and no otherwise. If no, then the tableau algorithm takes this as a contradiction and continues its search of the (abstract) solution space. The net result is that, provided the abstract part of the tableaux algorithm is sound and complete, and the oracle is sound and complete for the concrete value problem, then the algorithm is sound and complete for the overall problem. > 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. This entailment holds if: intersectionOf(complementOf(restriction(p allValuesFrom(xsd:string))) (restriction(p allValuesFrom(xsd:NMTOKEN)))) is unsatisfiable. This will result in the tableau algorithm asking the oracle if there exists some y s.t. xsd:NMTOKEN(y) and not xsd:string(y) is satisfiable. Assuming the oracle answers no, then the algorithm will return unsatisfiable. > > Please confirm that I need to read more carefully! Confirmed. To be fair, Jeff is still in the process of refining the algorithm. If you ask him nicely I am sure he will send you a more up to date version of that makes things a bit clearer. Ian > > Jeremy > > >Received on Wednesday, 29 January 2003 17:38:26 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:56:51 UTC
*