Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2016
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914741246492672 |
|---|---|
| author | Kieronski, Emanuel Tendera, Lidia |
| author_facet | Kieronski, Emanuel Tendera, Lidia |
| contents | We consider extensions of the two-variable guarded fragment, GF2, where distinguished binary predicates that occur only in guards are required to be interpreted in a special way (as transitive relations, equivalence relations, pre-orders or partial orders). We prove that the only fragment that retains the finite (exponential) model property is GF2 with equivalence guards without equality. For remaining fragments we show that the size of a minimal finite model is at most doubly exponential. 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. We improve the bounds and obtain optimal ones for all the fragments considered, in particular NExpTime for GF2 with equivalence guards, and 2ExpTime for GF2 with transitive guards. To obtain our results we essentially use some results from integer programming. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1611_03267 |
| institution | arXiv |
| publishDate | 2016 |
| record_format | arxiv |
| spellingShingle | Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants Kieronski, Emanuel Tendera, Lidia Logic in Computer Science We consider extensions of the two-variable guarded fragment, GF2, where distinguished binary predicates that occur only in guards are required to be interpreted in a special way (as transitive relations, equivalence relations, pre-orders or partial orders). We prove that the only fragment that retains the finite (exponential) model property is GF2 with equivalence guards without equality. For remaining fragments we show that the size of a minimal finite model is at most doubly exponential. 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. We improve the bounds and obtain optimal ones for all the fragments considered, in particular NExpTime for GF2 with equivalence guards, and 2ExpTime for GF2 with transitive guards. To obtain our results we essentially use some results from integer programming. |
| title | Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/1611.03267 |