Tableaux for Hybrid XPath with Data

被引：2
|
作者：
Areces, Carlos [1 ,2 ]
Fervari, Raul [1 ,2 ]
Seiler, Nahuel [1 ]
机构：
[1] Univ Nacl Cordoba, FAMAF, Cordoba, Argentina
[2] Consejo Nacl Invest Cient & Tecn, Cordoba, Argentina
来源：
PROGRESS IN ARTIFICIAL INTELLIGENCE (EPIA 2017) | 2017年 / 10423卷
基金：
欧盟地平线“2020”;
关键词：
XPath; Hybrid logic; Tableaux; Termination; Complexity;
D O I：
10.1007/978-3-319-65340-2_50
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We provide a sound, complete and terminating tableau procedure to check satisfiability of downward XPath=formulas enriched with nominals and satisfaction operators. The calculus is inspired by ideas introduced to ensure termination of tableau calculi for certain Hybrid Logics. We prove that even though we increased the expressive power of XPath by introducing hybrid operators, the satisfiability problem for the obtained logic is still PSpace-complete.
引用
收藏
页码：611 / 623
页数：13
相关论文
共 50 条
  • [1] AXIOMATIZING HYBRID XPATH WITH DATA
    Areces, Carlos
    Fervari, Raul
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (03) : 5:1 - 5:37
  • [2] Hilbert-Style Axiomatization for Hybrid XPath with Data
    Areces, Carlos
    Fervari, Raul
    [J]. LOGICS IN ARTIFICIAL INTELLIGENCE, (JELIA 2016), 2016, 10021 : 34 - 48
  • [3] Lightweight hybrid tableaux
    Hoffmann, Guillaume
    [J]. JOURNAL OF APPLIED LOGIC, 2010, 8 (04) : 397 - 408
  • [4] Data Driven XPath Generation
    De Mol, Robin
    Bronselaer, Antoon
    Nielandt, Joachim
    De Tre, Guy
    [J]. INTELLIGENT SYSTEMS'2014, VOL 1: MATHEMATICAL FOUNDATIONS, THEORY, ANALYSES, 2015, 322 : 569 - 580
  • [5] Clausal Tableaux for Hybrid PDL
    Kaminski, Mark
    Smolka, Gert
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 278 : 99 - 113
  • [6] Hybrid Tableaux for the Difference Modality
    Kaminski, Mark
    Smolka, Gert
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 231 : 241 - 257
  • [7] Axiomatizations for downward XPath on data trees
    Abriola, Sergio
    Emilia Descotte, Maria
    Fervari, Raul
    Figueira, Santiago
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2017, 89 : 209 - 245
  • [8] An extension of data automata that captures xpath
    Warsaw University, Poland
    [J]. Log. Methods Comp. Sci, 1
  • [9] AN EXTENSION OF DATA AUTOMATA THAT CAPTURES XPATH
    Bojanczyk, Mikolaj
    Lasota, Slawomir
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (01)
  • [10] Terminating Tableaux for Hybrid Logic with Eventualities
    Kaminski, Mark
    Smolka, Gert
    [J]. AUTOMATED REASONING, 2010, 6173 : 240 - 254
12345