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 条
  • [1] ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse
    Linh Anh Nguyen
    Szalas, Andrzej
    STUDIA LOGICA, 2011, 98 (03) : 387 - 428
  • [2] ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse
    Linh Anh Nguyen
    Andrzej Szałas
    Studia Logica, 2011, 98 : 387 - 428
  • [3] A tableau calculus with automaton-labelled formulae for regular grammar logics
    Goré, R
    Nguyen, LA
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 2005, 3702 : 138 - 152
  • [4] On the Horn Fragments of Serial Regular Grammar Logics with Converse
    Linh Anh Nguyen
    Szalas, Andrzej
    ADVANCED METHODS AND TECHNOLOGIES FOR AGENT AND MULTI-AGENT SYSTEMS, 2013, 252 : 225 - 234
  • [5] Deciding Regular Grammar Logics with Converse Through First-Order Logic
    Stéphane Demri
    Hans De Nivelle
    Journal of Logic, Language and Information, 2005, 14 (3) : 289 - 329
  • [6] A fibred tableau calculus for modal logics of agents
    Padmanabhan, Vineet
    Governatori, Guido
    DECLARATIVE AGENT LANGUAGES AND TECHNOLOGIES IV, 2006, 4237 : 105 - +
  • [7] A tableau calculus for multimodal logics and some (un)decidability results
    Baldoni, M
    Giordano, L
    Martelli, A
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1998, 1397 : 44 - 59
  • [8] A Tableau Calculus for Non-Clausal Regular MaxSAT
    Coll, Jordi
    Li, Chu Min
    Manya, Felip
    Yangin, Elifnaz
    2024 IEEE 54TH INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC, ISMVL 2024, 2024, : 137 - 142
  • [9] Tableau Calculus for Preference-Based Conditional Logics: PCL and its Extensions
    Giordano, Laura
    Gliozzi, Valentina
    Olivetti, Nicola
    Schwind, Camilla
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2009, 10 (03)
  • [10] The disconnection tableau calculus
    Letz, Reinhold
    Stenz, Gernot
    Journal of Automated Reasoning, 2007, 38 (1-3): : 79 - 126
12345