Finite satisfiability of the two-variable guarded fragment with transitive guards and related variants

DOI10.1145/3174805zbMATH Open1407.03009arXiv1611.03267OpenAlexW2571435091MaRDI QIDQ4608732FDOQ4608732

Authors: Emanuel Kieroński, Lidia Tendera 

Publication date: 22 March 2018

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1611.03267

Recommendations

• On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards
• On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity
• Computer Science Logic
• scientific article; zbMATH DE number 1956520
• Equivalence closure in the two-variable guarded fragment

zbMATH Keywords

computational complexityequivalence relationtwo-variable logicguarded fragmenttransitive relationfinite satisfiability problem

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Model theory of finite structures (03C13) Decidability of theories and sets of sentences (03B25)

Cited In (14)

• Highly acyclic groups, hypergraph covers, and the guarded fragment
• Title not available (Why is that?)
• Title not available (Why is that?)
• Finite Conformal Hypergraph Covers and Gaifman Cliques in Finite Structures
• The fluted fragment with transitive relations
• On the complexity of the two-variable guarded fragment with transitive guards
• On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards
• Equivalence closure in the two-variable guarded fragment
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity
• Finite model theory of the triguarded fragment and related logics
• Finite satisfiability for two‐variable, first‐order logic with one transitive relation is decidable
• Computer Science Logic

This page was built for publication: Finite satisfiability of the two-variable guarded fragment with transitive guards and related variants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4608732)