Data-Aware Hybrid Tableaux

Areces, C., Cassano, V., and Fervari, R.. Data-Aware Hybrid Tableaux. Logical Methods in Computer Science, 2025. To appear

Download

[pdf] 

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.

BibTeX

@article{arec:data25,
  author = {Areces, C. and Cassano, V. and Fervari, R.},
  title = {Data-Aware Hybrid Tableaux},
  journal = {Logical Methods in Computer Science},
  note = {To appear},
  year = 2025,
  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.",
  issn = "1860-5974",
}