Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Data-Aware Hybrid Tableaux

Carlos Areces, Valentin Cassano, Raul Fervari

TL;DR

The paper develops an internalized, data-aware tableau calculus for XPath_D augmented with hybrid logic features (nominals and satisfiability modalities) to reason about data-valued paths. It proves soundness, completeness, and termination, and shows that satisfiability for HXPath_D is PSPACE-complete, with a polynomial-space algorithm suitable for implementation. Extensions handle data trees/forests, as well as pure axioms and node-creating rules to capture more model classes and operators. The framework provides a foundation for practical reasoning about semi-structured data queries and paves the way for applying hybrid-tableau techniques to related data-aware logics.

Abstract

Labelled tableaux have been a traditional approach to define satisfiability checking procedures for Modal Logics. In many cases, they can also be used to obtain tight complexity bounds and lead to efficient implementations of reasoning tools. More recently, it has been shown that the expressive power provided by the operators characterizing Hybrid Logics (nominals and satisfiability modalities) can be used to internalize labels, leading to well-behaved inference procedures for fairly expressive logics. The resulting procedures are attractive because they do not use external mechanisms outside the language of the logic at hand, and have good logical and computational properties. Many tableau systems based on Hybrid Logic have been investigated, with more recent efforts concentrating on Modal Logics that support data comparison operators. Here, we introduce an internalized tableau calculus for XPath, arguably one of the most prominent approaches for querying semistructured data. More precisely, we define data-aware tableaux for XPath featuring data comparison operators and enriched with nominals and the satisfiability modalities from Hybrid Logic. We prove that the calculus is sound, complete and terminating. Moreover, we show that tableaux can be explored in polynomial space, therefore establishing that the satisfiability problem for the logic is PSpace-complete. Finally, we explore different extensions of the calculus, in particular how to handle data trees and other frame classes.

Data-Aware Hybrid Tableaux

TL;DR

The paper develops an internalized, data-aware tableau calculus for XPath_D augmented with hybrid logic features (nominals and satisfiability modalities) to reason about data-valued paths. It proves soundness, completeness, and termination, and shows that satisfiability for HXPath_D is PSPACE-complete, with a polynomial-space algorithm suitable for implementation. Extensions handle data trees/forests, as well as pure axioms and node-creating rules to capture more model classes and operators. The framework provides a foundation for practical reasoning about semi-structured data queries and paves the way for applying hybrid-tableau techniques to related data-aware logics.

Abstract

Labelled tableaux have been a traditional approach to define satisfiability checking procedures for Modal Logics. In many cases, they can also be used to obtain tight complexity bounds and lead to efficient implementations of reasoning tools. More recently, it has been shown that the expressive power provided by the operators characterizing Hybrid Logics (nominals and satisfiability modalities) can be used to internalize labels, leading to well-behaved inference procedures for fairly expressive logics. The resulting procedures are attractive because they do not use external mechanisms outside the language of the logic at hand, and have good logical and computational properties. Many tableau systems based on Hybrid Logic have been investigated, with more recent efforts concentrating on Modal Logics that support data comparison operators. Here, we introduce an internalized tableau calculus for XPath, arguably one of the most prominent approaches for querying semistructured data. More precisely, we define data-aware tableaux for XPath featuring data comparison operators and enriched with nominals and the satisfiability modalities from Hybrid Logic. We prove that the calculus is sound, complete and terminating. Moreover, we show that tableaux can be explored in polynomial space, therefore establishing that the satisfiability problem for the logic is PSpace-complete. Finally, we explore different extensions of the calculus, in particular how to handle data trees and other frame classes.
Paper Structure (16 sections, 25 theorems, 24 equations, 9 figures, 2 algorithms)

This paper contains 16 sections, 25 theorems, 24 equations, 9 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Organization.
  4. Preliminaries
  5. Tableaux for $\mathsf{HXPath_D}\xspace$
  6. Tableau Calculus.
  7. Soundness
  8. Completeness
  9. Termination
  10. Complexity of the Satisfiability Problem for $\mathsf{HXPath_D}\xspace$
  11. Forest and Tree Models
  12. Pure Axioms and Node Creating Rules
  13. Pure Axioms
  14. Node Creating Rules
  15. Final Remarks
  16. ...and 1 more sections

Key Result

Proposition 2.4

Let $\mathfrak{M}$ be any model. The following node expressions are valid in $\mathfrak{M}$:

Figures (9)

  • Figure 1: An example of a data tree.
  • Figure 2: Basic Rules
  • Figure 3: Rules for Nominals
  • Figure 4: Rules for Internalizing Nominals and Negations into Data (In)Equalities
  • Figure 5: Rules for Handling Path Expressions in Data (In)Equalities
  • ...and 4 more figures

Theorems & Definitions (77)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Proposition 2.4
  • Definition 3.1
  • Example 3.2
  • Definition 3.3
  • Definition 3.4
  • Definition 3.5
  • Lemma 3.6
  • ...and 67 more