LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Proof Theory for XPath using Hybrid Logic tools
- Date
- Tuesday, July 11 2017 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Raul Fervari (FaMAF-Universidad Nacional de Córdoba, and CONICET, Argentina)
XPath is arguably the most widely used XML query language. It is fundamentally a general purpose language for addressing, searching, and matching pieces of an XML document. The navigational fragment of XPath, known as Core-XPath is essentially a modal logic, since it allows us to describe structural properties of relational models, i.e., of XML documents (see e.g. [1]). However, without the ability to relate nodes based on the actual data values of the attributes, the logic’s expressive power is inappropriate for many applications. The extension of Core-XPath with (in)equality tests between attributes of elements in an XML document, named Core-Data-XPath (here XPath=) is more appropriate in some of these situations. Recent articles also investigate XPath= from a modal perspective.
In this talk I will start by motivating the use of XPath=. Then we will discuss proof systems for XPath=, and will present and motivate our approach. The main idea is that we extend XPath= with nominals and the hybrid operator @ to take advantage of tools used in proof theory for Hybrid Logic. We focus in the definition of an Hilbert-style axiomatic system [2] for this logic, whose completeness proof is based in a Henkin-style construction. Finally we will discuss a similar idea for defining a terminating tableaux calculus for the same logic [3], before concluding with future directions.