6533b824fe1ef96bd1280108

RESEARCH PRODUCT

Two-Variable First-Order Logic with Equivalence Closure

Ian Pratt-hartmannLidia TenderaEmanuel KieronskiJakub Michaliszyn

subject

Discrete mathematicsGeneral Computer ScienceLogical equivalenceFinite model propertyGeneral MathematicsDescriptive complexity theorySatisfiabilityDecidabilityFirst-order logicCombinatoricsTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESComputer Science::Logic in Computer ScienceMaximum satisfiability problemClosure operatorEquivalence relationBoolean satisfiability problemMathematics

description

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.

yearjournalcountryeditionlanguage
2012-06-012012 27th Annual IEEE Symposium on Logic in Computer Science
https://doi.org/10.1109/lics.2012.53