zbMATH — the first resource for mathematics

A sequent calculus for a modal logic on finite data trees. (English) Zbl 1370.03043
Regnier, Laurent (ed.) et al., 25th EACSL annual conference and 30th workshop on computer science logic, CSL’16, Marseille, France, August 29 – September 1, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-022-4). LIPIcs – Leibniz International Proceedings in Informatics 62, Article 32, 16 p. (2016).
Summary: We investigate the proof theory of a modal fragment of XPath equipped with data (in)equality tests over finite data trees, i.e., over finite unranked trees where nodes are labelled with both a symbol from a finite alphabet and a single data value from an infinite domain. We present a sound and complete sequent calculus for this logic, which yields the optimal PSPACE complexity bound for its validity problem.
For the entire collection see [Zbl 1351.68028].

03B70 Logic in computer science
03B45 Modal logic (including the logic of norms)
03F05 Cut-elimination and normal-form theorems
68P05 Data structures
68Q25 Analysis of algorithms and problem complexity
Full Text: DOI