Sequent Calculi for Data-Aware Modal Logics
Carlos Areces, Valentin Cassano, Danae Dutto, Raul Fervari
TL;DR
This paper introduces a Gentzen-style sequent calculus for HXPathD, providing detailed formal proofs of its soundness, completeness, invertibility, and cut elimination, serving as a comprehensive technical reference.
Contribution
It presents a new formal sequent calculus for HXPathD with rigorous proofs of key logical properties, enhancing understanding of data-aware modal logics.
Findings
Proves soundness and completeness of the calculus
Establishes invertibility and cut elimination
Provides detailed formal proofs and technical details
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.