Variable-free reasoning on finite
trees
Vendredi 7 novembre 2003 à 14 heures
Bureau 314 de l'Irit
Résumé : Reasoning about finite
ordered trees is becoming very important with the advent of the new data
storage format XML. XPath is the most widely used language to retrieve data
from XML documents. We show the close connection between XPath and various
well investigated variable free formalisms interpreted on trees:
Kleene algebras
with tests, propositional dynamic logic, since/until temporal logic. We present
an extension of XPath which can express all first-order definable queries
over ordered trees. We give a linear time algorithm for query evaluation
for a language which extends XPath with all regular expressions and tests
over the four basic axes. We give an EXPTIME decision algorithm which can
be used to decide equivalence of a large number of XPath expressions given
a set of constraints (eg, an XML schema definition or a document type
definition
(DTD).
Retour a la page
des seminaires