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 条

[31] The first-order theory of binary overlap-free words is decidable
Schaeffer, Luke
Shallit, Jeffrey
[J]. CANADIAN JOURNAL OF MATHEMATICS-JOURNAL CANADIEN DE MATHEMATIQUES, 2023,
[32] Monodic Fragments of Probabilistic First-Order Logic
Jung, Jean Christoph
Lutz, Carsten
Goncharov, Sergey
Schroeder, Lutz
[J]. AUTOMATA, LANGUAGES, AND PROGRAMMING (ICALP 2014), PT II, 2014, 8573 : 256 - 267
[33] Lindstrom theorems for fragments of first-order logic
ten Cate, Balder
van Benthem, Johan
Vaeaenaenen, Jouko
[J]. 22ND ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2007, : 280 - +
[34] LINDSTROM THEOREMS FOR FRAGMENTS OF FIRST-ORDER LOGIC
Van Benthem, Johan
Ten Cate, Balder
Vaananen, Jouko
[J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2009, 5 (03)
[35] On first-order fragments for words and Mazurkiewicz traces
Diekert, Volker
Kufleitner, Manfred
[J]. DEVELOPMENTS IN LANGUAGE THEORY, PROCEEDINGS, 2007, 4588 : 1 - +
[36] UNIFORM INTERPOLATION LEMMA FOR FIRST-ORDER LOGIC WITH EQUALITY
WEAVER, GE
[J]. NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1972, 19 (04): : A535 - &
[37] UNIFORM COMPACTNESS AND INTERPOLATION LEMMAS IN FIRST-ORDER LOGIC
WEAVER, G
[J]. JOURNAL OF SYMBOLIC LOGIC, 1974, 39 (02) : 394 - 394
[38] Interpolation theory and first-order boundary value problems
Everitt, WN
Poulkou, A
[J]. MATHEMATISCHE NACHRICHTEN, 2004, 269 : 116 - 128
[39] Decidable first-order theories of one-step rewriting in trace monoids
Kuske, D
Lohrey, M
[J]. THEORY OF COMPUTING SYSTEMS, 2005, 38 (01) : 39 - 81
[40] Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Heuer, Jan
Wernhard, Christoph
[J]. AUTOMATED REASONING, IJCAR 2024, PT I, 2024, 14739 : 172 - 193

← 1 2 3 4 5 →