Complete axiomatizations for XPath fragments

13 years 5 months ago
Complete axiomatizations for XPath fragments
We provide complete axiomatizations for several fragments of XPath: sets of equivalences from which every other valid equivalence is derivable. Specifically, we axiomatize downward single axis fragments of Core XPath (that is, Core XPath(↓) and Core XPath(↓+ )) as well as the full Core XPath. We make use of techniques from modal logic. XPath is a language for navigating through XML documents. In this paper, we consider the problem of finding complete axiomatizations for fragments of XPath. By an axiomatization we mean a finite set of valid equivalences between XPath expressions. These equivalences can be thought of as (undirected) rewrite rules. Completeness then means that any two equivalent expressions can be rewritten to each other using the given equivalences. Completeness tells us, in a mathematically precise way, that the given set of equivalences captures everything there is to say about semantic equivalence of XPath expressions. We are aware of two complete axiomatizatio...
Balder ten Cate, Tadeusz Litak, Maarten Marx
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Authors Balder ten Cate, Tadeusz Litak, Maarten Marx
Comments (0)