On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards
On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards
复制标题
关于具有等价或传递保护的保护片段的有限可满足性
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Lidia Tendera
中科院分区：
文献类型：
--
作者：
Emanuel Kieronski;Lidia Tendera
一阶逻辑的保护片段GF具有有限模型性质，因此可满足性问题与有限可满足性问题是一致的。
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.