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.