On the Mints Hierarchy in First-Order Intuitionistic Logic

被引：7

作者：

Schubert, Aleksy ^{[1
]}

Urzyczyn, Pawel ^{[1
]}

Zdanowski, Konrad ^{[2
]}

机构：

[1] Univ Warsaw, Inst Informat, PL-02097 Warsaw, Poland

[2] Cardinal Stefan Wyszynski Univ Warsaw, PL-01815 Warsaw, Poland

来源：

FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2015) | 2015年 / 9034卷

关键词：

INTERSECTION TYPES; PREDICATE LOGIC; DECIDABILITY; INHABITATION;

D O I：

10.1007/978-3-662-46678-0_29

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We study the decidability and complexity of fragments of intuitionistic first-order logic over (for all, ->) determined by the alternation of positive and negative occurrences of quantifiers (Mints hierarchy). We prove that fragments Pi(2) and Sigma(2) are undecidable and that Sigma(1) is EXPSPACE-complete.

引用

页码：451 / 465

页数：15

共 23 条

[1]

[Anonymous], 2012, The Coq proof assistant reference manual

[2]

[Anonymous], 1997, Perspectives in Mathematical Logic

[3]

Bonevac Daniel, 2012, HDB HIST LOGIC, V11

[4]

Bove A, 2009, LECT NOTES COMPUT SC, V5674, P73, DOI 10.1007/978-3-642-03359-9_6