T.: Efficient reasoning about XFDs with pre-image semantics

Abstract. The study of integrity constraints has been identified as one of the major challenges in XML database research. The main difficulty is finding a balance between the expressiveness and the existence of auto-mated reasoning tools. We investigate a previous proposal for functional dependencies in XML (XFDs) that is based on homomorphisms between data trees and schema trees. We demonstrate that reasoning about our XFDs is well-founded. We provide a finite axiomatisation and show that their implication is equivalent to the logical implication of propositional Horn clauses and thus decidable in time linear in the size of the con-straints. Hence, our XFDs do not only capture valuable semantic infor-mation but also permit efficient automated reasoning support.