Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Sequent Calculi for Data-Aware Modal Logics

Carlos Areces, Valentin Cassano, Danae Dutto, Raul Fervari

TL;DR

The paper develops a Gentzen-style sequent calculus for the data-aware hybrid XPath logic $\text{HXPath}_{\rm D}$, formalizing both the syntax and a semantic hybrid-data model. It establishes soundness, invertibility, and completeness of the calculus, linking it to the Hilbert-style system and ArecesF21, and proves cut elimination to yield a robust, cut-free proof system. The work provides a rigorous foundation for reasoning about data-aware modal logics with nominals, modalities, and data comparisons, enabling formal verification and automated reasoning in data-rich XML-like settings.

Abstract

This document serves as a companion to the paper of the same title, wherein we introduce a Gentzen-style sequent calculus for HXPathD. It provides full technical details and proofs from the main paper. As such, it is intended as a reference for readers seeking a deeper understanding of the formal results, including soundness, completeness, invertibility, and cut elimination for the calculus.

Sequent Calculi for Data-Aware Modal Logics

TL;DR

The paper develops a Gentzen-style sequent calculus for the data-aware hybrid XPath logic , formalizing both the syntax and a semantic hybrid-data model. It establishes soundness, invertibility, and completeness of the calculus, linking it to the Hilbert-style system and ArecesF21, and proves cut elimination to yield a robust, cut-free proof system. The work provides a rigorous foundation for reasoning about data-aware modal logics with nominals, modalities, and data comparisons, enabling formal verification and automated reasoning in data-rich XML-like settings.

Abstract

This document serves as a companion to the paper of the same title, wherein we introduce a Gentzen-style sequent calculus for HXPathD. It provides full technical details and proofs from the main paper. As such, it is intended as a reference for readers seeking a deeper understanding of the formal results, including soundness, completeness, invertibility, and cut elimination for the calculus.

Paper Structure

This paper contains 9 sections, 8 theorems, 4 equations, 3 figures.

Table of Contents

  1. Hybrid XPath with Data
  2. A Sequent Calculus for $\text{\rm HXPath}_{\rm D}$
  3. Soundness
  4. Invertibility
  5. Derived Rules
  6. Completeness
  7. Base Case.
  8. Inductive Case.
  9. Cut Elimination

Key Result

Proposition 4

[proposition]prop:abbrv $\amodel,n \Vdash \langle\alpha\rangle\varphi$ iff $\hbox{exists $n' \in \mathrm{N}$ s.t.},~ \amodel,n,n' \Vdash\alpha$ and $\amodel,n' \Vdash \varphi$. Moreover, $\amodel,n \Vdash [\alpha=_{\xspace\mathsf{c}\xspace}\beta]$ iff for all $n',n"\in \mathrm{N}$, $\amodel,n,n' \Vd

Figures (3)

  • Figure 1: Axioms System $\mathbf{H}$ for $\text{\rm HXPath}_{\rm D}$
  • Figure 2: Sequent Calculus $\mathbf{G}$ for $\text{\rm HXPath}_{\rm D}$.
  • Figure 3: Derived Sequent Rules for $\text{\rm HXPath}_{\rm D}$.

Theorems & Definitions (25)

  • Definition 1
  • Definition 2
  • Definition 3
  • Proposition 4
  • Definition 5
  • Remark 1
  • Theorem 6: Soundness and Completeness ArecesF21
  • Definition 7
  • Definition 8
  • Definition 9
  • ...and 15 more