Details

Autor(en) / Beteiligte

• Kieroński, Emanuel
• Michaliszyn, Jakub
• Pratt-Hartmann, Ian
• Tendera, Lidia

Titel

Two-Variable First-Order Logic with Equivalence Closure

Ist Teil von

• SIAM journal on computing, 2014-01, Vol.43 (3), p.1012-1063

Ort / Verlag

Philadelphia: Society for Industrial and Applied Mathematics

Erscheinungsjahr

2014

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• We consider the satisfiability and finite satisfiability problems for extensions of the two-variable fragment of first-order logic in which an equivalence closure operator can be applied to a fixed number of binary predicates. We show that the satisfiability problem for two-variable, first-order logic with equivalence closure applied to two binary predicates is in 2-NExpTime, and we obtain a matching lower bound by showing that the satisfiability problem for two-variable first-order logic in the presence of two equivalence relations is 2-NExpTime-hard. The logics in question lack the finite model property; however, we show that the same complexity bounds hold for the corresponding finite satisfiability problems. We further show that the satisfiability (${=}$ finite satisfiability) problem for the two-variable fragment of first-order logic with equivalence closure applied to a single binary predicate is NExpTime-complete. [PUBLICATION ABSTRACT]