文章基本信息

标题：A Sequent Calculus for a Modal Logic on Finite Data Trees
本地全文：下载
作者：David Baelde ; Simon Lunel ; Sylvain Schmitz 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2016
卷号：62
页码：32:1-32:16
DOI：10.4230/LIPIcs.CSL.2016.32
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：XPath; proof systems; modal logic; complexity