- From: Ian Horrocks <horrocks@cs.man.ac.uk>
- Date: Wed, 29 Jan 2003 22:37:39 +0000
- 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