6533b826fe1ef96bd1283b13

RESEARCH PRODUCT

On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards

Emanuel KieronskiLidia Tendera

subject

Discrete mathematicsTransitive relationFinite model propertyDouble exponential functionEquivalence (formal languages)AlgorithmSatisfiabilityFinite satisfiabilityMathematics

description

The guarded fragment of first-order logic, GF, enjoys the finite model property, so the satisfiability and the finite satisfiability problems coincide. We are concerned with two extensions of the two-variable guarded fragment that do not possess the finite model property, namely, GF2 with equivalence and GF2 with transitive guards. We prove that in both cases every finitely satisfiable formula has a model of at most double exponential size w.r.t. its length. To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2NEXPTIME-upper bound on the complexity of the finite satisfiability problem for these fragments. For the case with equivalence guards we improve the bound to 2EXPTIME.

yearjournalcountryeditionlanguage
2007-10-06
https://doi.org/10.1007/978-3-540-75560-9_24