Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Proof Theory for XPath using Hybrid Logic tools

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Raul Fervari
Date
Le mardi 11 juillet 2017 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
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.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents