@INPROCEEDINGS{VionDury03,
   AUTHOR = {Jean-Yves Vion-Dury and Nabil Laya\"ida},
   TITLE = {Containment of {XPath} expressions: an Inference and Rewriting based approach},
   BOOKTITLE = {Extreme Markup Languages},
   PUBLISHER = {IDEAlliance},
   LOCATION = {Montr\'eal, Canada},
   MONTH = AUG,
   YEAR = 2003,
   URL = {http://wam.inrialpes.fr/publications/2003/xtrem2003/xtrem2003.pdf},
   ABSTRACT = {XPath is a simple query language for XML documents which allows
    navigating in XML trees and returning a set of matching nodes. It is used
    in XML Schema to define keys an in XLink and XPointer to reference
    portions of documents. XPath is a fundamental part of XSLT and XQuery
    languages as it allows to define matching expressions for patterns and
    provides node selectors to filter elements in the transformations.
    We propose to study the containment and equivalence of XPath expressions
    using an inference system combined with a rewriting system. The inference
    system allows to assert and prove properties on a class of expressions.
    In order to keep the proof system compact, we propose a re-writing
    architecture which allows to transform remaining expressions in a
    disjunctive normal form compatible with this class. In contrast with
    model based approaches, the inference and rewriting systems are applied
    to the XPath language directly. We believe this will help understanding
    the underlying issues of deciding containment on the language itself.}
}