S.: Unlocking keys for XML trees

Abstract. We review key constraints in the context of XML as intro-duced by Buneman et al. We show that one of the proposed inference rules is not sound in general, and the axiomatisation proposed for XML keys is incomplete even if key paths are simple. Therefore, the axiomati-sation and also the implication problem for XML keys are still unsolved. We propose a set of inference rules that is indeed sound and complete for the implication of XML keys with simple key paths. Our complete-ness proof enables us to characterise the implication of XML keys in terms of the reachability problem of nodes in a digraph. This results in a quadratic time algorithm for deciding XML key implication, and shows that reasoning for XML keys is practically efficient.