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
AMBLER, S
KWIATKOWSKA, M
MEASOR, N
[J]. 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
Baelde, David
[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2012, 13 (01)
[6] Sahlqvist theorem for modal fixed point logic
Bezhanishvili, Nick
Hodkinson, Ian
[J]. THEORETICAL COMPUTER SCIENCE, 2012, 424 : 1 - 19
[7] Epistemic logics for sceptical agents
Bilkova, Marta
Majer, Ondrej
Pelis, Michal
[J]. 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 →