The Fluted Fragment with Transitivity

Ian Pratt-Hartmann; Lidia Tendera

doi:10.4230/LIPIcs.MFCS.2019.18

The Fluted Fragment with Transitivity

Ian Pratt-Hartmann, Lidia Tendera

Formal Methods

Uniwersytet Opolski

Research output: Contribution to conference › Paper › peer-review

Abstract

We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

Original language	English
Pages	18:1-18:15
Number of pages	15
DOIs	https://doi.org/10.4230/LIPIcs.MFCS.2019.18
Publication status	Published - 20 Aug 2019
Event	44th International Symposium on Mathematical Foundations of Computer Science - Aachen, Germany Duration: 26 Aug 2019 → 30 Aug 2019

Conference

Conference	44th International Symposium on Mathematical Foundations of Computer Science
Abbreviated title	MFCS 2019
Country/Territory	Germany
City	Aachen
Period	26/08/19 → 30/08/19

Keywords

First-Order logic
Decidability
Satisfiability
Transitivity
Complexity

Access to Document

10.4230/LIPIcs.MFCS.2019.18Licence: CC BY

Cite this

@conference{0a8a3588be3d41b985af8c471a8249e6,

title = "The Fluted Fragment with Transitivity",

abstract = "We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.",

keywords = "First-Order logic, Decidability, Satisfiability, Transitivity, Complexity",

author = "Ian Pratt-Hartmann and Lidia Tendera",

year = "2019",

month = aug,

day = "20",

doi = "10.4230/LIPIcs.MFCS.2019.18",

language = "English",

pages = "18:1--18:15",

note = "44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019 ; Conference date: 26-08-2019 Through 30-08-2019",

}

TY - CONF

T1 - The Fluted Fragment with Transitivity

AU - Pratt-Hartmann, Ian

AU - Tendera, Lidia

PY - 2019/8/20

Y1 - 2019/8/20

N2 - We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

AB - We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

KW - First-Order logic

KW - Decidability

KW - Satisfiability

KW - Transitivity

KW - Complexity

U2 - 10.4230/LIPIcs.MFCS.2019.18

DO - 10.4230/LIPIcs.MFCS.2019.18

M3 - Paper

SP - 18:1-18:15

T2 - 44th International Symposium on Mathematical Foundations of Computer Science

Y2 - 26 August 2019 through 30 August 2019

ER -

The Fluted Fragment with Transitivity

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this