Constructive Canonicity for Lattice-Based Fixed Point Logics

被引：10

作者：

Conradie, Willem ^{[1
]}

Craig, Andrew ^{[1
]}

Palmigiano, Alessandra ^{[1
,2
]}

Zhao, Zhiguang ^{[2
]}

机构：

[1] Univ Johannesburg, Dept Pure & Appl Math, Johannesburg, South Africa

[2] Delft Univ Technol, Fac Technol Policy & Management, Delft, Netherlands

来源：

LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION: 24TH INTERNATIONAL WORKSHOP, WOLLIC 2017, LONDON, UK, JULY 18-21, 2017, PROCEEDINGS | 2017年 / 10388卷

基金：

新加坡国家研究基金会;

关键词：

Canonicity; Lattice-based fixed point logics; Logics for categorization; Unified correspondence; MODAL MU-CALCULUS; ALGORITHMIC CORRESPONDENCE; SAHLQVIST THEORY; COMPLETENESS; PROOF;

D O I：

10.1007/978-3-662-55386-2_7

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.

引用

页码：92 / 109

页数：18

共 29 条

[1] DUALITY AND THE COMPLETENESS OF THE MODAL MU-CALCULUS [J].

AMBLER, S ;

KWIATKOWSKA, M ;

MEASOR, N .

THEORETICAL COMPUTER SCIENCE, 1995, 151 (01) :3-27

[2]

[Anonymous], ARXIV160308515

[3]

[Anonymous], ARXIV160306547

[4]

[Anonymous], ARXIV160308341

[5] Least and Greatest Fixed Points in Linear Logic [J].

Baelde, David .

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2012, 13 (01)

[6] Sahlqvist theorem for modal fixed point logic [J].

Bezhanishvili, Nick ;

Hodkinson, Ian .

THEORETICAL COMPUTER SCIENCE, 2012, 424 :1-19

[7] Epistemic logics for sceptical agents [J].

Bilkova, Marta ;

Majer, Ondrej ;

Pelis, Michal .

JOURNAL OF LOGIC AND COMPUTATION, 2016, 26 (06) :1815-1841

[8]

Britz C., 2016, THESIS

[9]

Conradie W., 2017, EPISTEMIC LOGI UNPUB

[10]

Conradie W., ARXIV151104271

← 1 2 3 →