Craig Interpolation for Decidable First-Order Fragments

被引：0

作者：

ten Cate, Balder ^{[1
]}

Comer, Jesse ^{[2
]}

机构：

[1] Univ Amsterdam, ILLC, NL-1098 XH Amsterdam, Netherlands

[2] Univ Penn, Philadelphia, PA 19104 USA

来源：

FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PT II, FOSSACS 2024 | 2024年 / 14575卷

关键词：

Craig interpolation; Decidability; Abstract model theory; THEOREM; LIMITS;

D O I：

10.1007/978-3-031-57231-9_7

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We show that the guarded-negation fragment (GNFO) is, in a precise sense, the smallest extension of the guarded fragment (GFO) with Craig interpolation. In contrast, we show that the smallest extension of the two-variable fragment (FO2), and of the forward fragment (FF) with Craig interpolation, is full first-order logic. Similarly, we also show that all extensions of FO2 and of the fluted fragment (FL) with Craig interpolation are undecidable.

引用

页码：137 / 159

页数：23

共 50 条

[1] Craig Interpolation for Decidable Fragments of First-Order Logic
ten Cate, Balder
[J]. 32ND EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC, CSL 2024, 2024, 288
[2] Decidable fragments of first-order temporal logics
Hodkinson, I
Wolter, F
Zakharyaschev, M
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2000, 106 (1-3) : 85 - 134
[3] Decidable fragments of first-order modal logics
Wolter, F
Zakharyaschev, M
[J]. JOURNAL OF SYMBOLIC LOGIC, 2001, 66 (03) : 1415 - 1438
[4] Craig Interpolation with Clausal First-Order Tableaux
Wernhard, Christoph
[J]. JOURNAL OF AUTOMATED REASONING, 2021, 65 (05) : 647 - 690
[5] Craig Interpolation with Clausal First-Order Tableaux
Christoph Wernhard
[J]. Journal of Automated Reasoning, 2021, 65 : 647 - 690
[6] Craig Interpolation with Clausal First-Order Tableaux
Wernhard, Christoph
[J]. Wernhard, Christoph (info@christophwerhard.com), 1600, Springer Science and Business Media B.V. (65): : 647 - 690
[7] Decidable and Undecidable Fragments of First-Order Concatenation Theory
Kristiansen, Lars
Murwanashyaka, Juvenal
[J]. SAILING ROUTES IN THE WORLD OF COMPUTATION, 2018, 10936 : 244 - 253
[8] Combinations of Theories for Decidable Fragments of First-Order Logic
Fontaine, Pascal
[J]. FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2009, 5749 : 263 - 278
[9] Decidable and undecidable fragments of first-order branching temporal logics
Hodkinson, I
Wolter, F
Zakharyaschev, M
[J]. 17TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2002, : 393 - 402
[10] The Craig interpolation property in first-order Gödel logic
Tavana, N. R.
Pourmahdian, M.
Khatami, S. M. A.
[J]. FUZZY SETS AND SYSTEMS, 2024, 485

← 1 2 3 4 5 →