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

DOI10.1145/3174805MaRDI QIDQ4608732zbMATH OpenOpenAlexFDO

Authors Emanuel Kieroński, Lidia Tendera

Publication date 22 March 2018

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

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

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)

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.

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

Cited in

(14)

• Highly acyclic groups, hypergraph covers, and the guarded fragment
• scientific article; zbMATH DE number 7566055 (Why is no real title available?)
• scientific article; zbMATH DE number 7561661 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 1956520 (Why is no real title available?)
• scientific article; zbMATH DE number 2086420 (Why is no real title available?)
• 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)