Decidable Elementary Modal Logics

被引：4

作者：

Michaliszyn, Jakub ^{[1
]}

Otop, Jan ^{[1
]}

机构：

[1] Univ Wroclaw, Inst Comp Sci, PL-51151 Wroclaw, Poland

来源：

2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) | 2012年

关键词：

modal logic; decidability; elementary logic;

D O I：

10.1109/LICS.2012.59

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper, the modal logic over classes of structures definable by universal first-order Horn formulas is studied. We show that the satisfiability problems for those logics are decidable, confirming the conjecture from [5]. We provide a full classification of logics defined by universal first-order Horn formulas, with respect to the complexity of satisfiability of modal formulas over the classes of frames they define. It appears, that except for the trivial case of inconsistent formulas for which the problem is in P, local satisfiability is either NP-complete or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete, or EXPTIME-complete. While our results hold even if we allow to use equality, we show that inequality leads to undecidability.

引用

页码：491 / 500

页数：10

共 14 条

[1]

[Anonymous], 2001, CAMBRIDGE TRACTS THE

[2] On the restraining power of guards [J].

Grädel, E .

JOURNAL OF SYMBOLIC LOGIC, 1999, 64 (04) :1719-1742

[3]

Gradel E., 1999, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), P45, DOI 10.1109/LICS.1999.782585

[4]

Hemaspaandra E., 1996, Notre Dame Journal of Formal Logic, V37, P174, DOI 10.1305/ndjfl/1040046086

[5]

Hemaspaandra E, 2008, STACS 2008: PROCEEDINGS OF THE 25TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE, P349

[6]

Hemaspaandra E, 2011, LECT NOTES COMPUT SC, V6907, P364, DOI 10.1007/978-3-642-22993-0_34

[7]

Kieronski E., 2012, LICS 12

[8] Modal Logics Definable by Universal Three-Variable Formulas [J].

Kieronski, Emanuel ;

Michaliszyn, Jakub ;

Otop, Jan .

IARCS ANNUAL CONFERENCE ON FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE (FSTTCS 2011), 2011, 13 :264-275

[9]

Ladner R. E., 1977, SIAM Journal on Computing, V6, P467, DOI 10.1137/0206033

[10]

Michaliszyn J, 2009, LECT NOTES COMPUT SC, V5556, P261, DOI 10.1007/978-3-642-02930-1_22

← 1 2 →