A Tableau Calculus for Regular Grammar Logics with Converse

被引：0
|
作者：
Nguyen, Linh Anh [1 ]
Szalas, Andrzej [1 ]
机构：
[1] Univ Warsaw, Inst Informat, PL-02097 Warsaw, Poland
来源：
AUTOMATED DEDUCTION - CADE-22 | 2009年 / 5663卷
关键词：
EXPTIME TABLEAUX;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We give a sound and complete tableau calculus for deciding the general satisfiability problem of regular grammar logics with converse (REG(c) logics). Tableaux of our calculus are defined as "and-or" graphs with global caching. Our calculus extends the tableau calculus for regular grammar logics given by Gore and Nguyen [11] by using a cut rule and existential automaton-modal operators to deal with converse. We use it to develop an ExPTIME (optimal) tableau decision procedure for the general satisfiability problem of REG(c) logics. We also briefly discuss optimizations for the procedure.
引用
收藏
页码：421 / 436
页数：16
相关论文
共 50 条
  • [41] On the undecidability of logics with converse, nominals, recursion and counting
    Bonatti, PA
    Peron, A
    ARTIFICIAL INTELLIGENCE, 2004, 158 (01) : 75 - 96
  • [42] Tableau Calculus for Basic Fuzzy Logic BL
    Kulacka, Agnieszka
    INFORMATION PROCESSING AND MANAGEMENT OF UNCERTAINTY IN KNOWLEDGE-BASED SYSTEMS, PT I, 2014, 442 : 325 - 334
  • [43] Flat modal fixpoint logics with the converse modality
    Enqvist, Sebastian
    JOURNAL OF LOGIC AND COMPUTATION, 2018, 28 (06) : 1065 - 1097
  • [44] A Tableau Calculus for Minimal Modal Model Generation
    Papacchini, Fabio
    Schmidt, Renate A.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 278 : 159 - 172
  • [45] Shortcuts and dynamic marking in the tableau method for adaptive logics
    Batens D.
    Meheus J.
    Studia Logica, 2001, 69 (2) : 221 - 248
  • [46] Tableau calculus for only knowing and knowing at most
    Rosati, R
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 2000, 1847 : 383 - 397
  • [47] The complexity of regularity in grammar logics and related modal logics
    Demri, S
    JOURNAL OF LOGIC AND COMPUTATION, 2001, 11 (06) : 933 - 960
  • [48] An analytic tableau calculus for a temporalised belief logic
    Ma, Ji
    Orgun, Mehmet A.
    Adi, Kamel
    JOURNAL OF APPLIED LOGIC, 2011, 9 (04) : 289 - 304
  • [49] CATEGORIAL GRAMMAR CALCULUS
    KARLGREN, H
    STATISTICAL METHODS IN LINGUISTICS, 1975, 1974 : 1 - 128
  • [50] Tableau reasoning for description logics and its extension to probabilities
    Zese, Riccardo
    Bellodi, Elena
    Riguzzi, Fabrizio
    Cota, Giuseppe
    Lamma, Evelina
    ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2018, 82 (1-3) : 101 - 130
12345