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...

• Type: Journal
• Year: 2010
• Where: JAPLL
• Authors: Balder ten Cate, Tadeusz Litak, Maarten Marx
• Keywords: Complete Axiomatizations, Core XPath, JAPLL 2010, XPath