arXiv subjects

Emanuel Kieroński

Publications and source records attributed to Emanuel Kieroński.

8 recordsLinked to original sources

arXiv2026

The Triguarded Fragment

A prominent research question in computational logic is how to restrict first-order predicate logic (FO) in such a way that the satisfiability problem becomes decidable. Among others, past efforts have identified two prominent decidable FO fragments of high expressivity: the guarded fragment (GF), and the two-variable fragment (FO2). These fragments are of high interest and crucial importance as they provide significant insights into decidability and expressiveness of other prominent (computational) logics like Modal Logics (MLs)} and various Description Logics (DLs)}, which play a central role in Verification, Knowledge Representation, and other areas. In this article, we show that GF and FO2 can be combined into a new fragment that subsumes both, while maintaining decidability of the satisfiability problem. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF by requiring guardedness of quantification only for subformulae with three or more free variables. We show that, when restricting the use of equality, satisfiability in TGF is N2ExpTime-complete, dropping to NExpTime-complete when the maximum predicate arity is fixed (a natural assumption in the context of MLs and DLs). We further establish that the problem is NP-complete in terms of data complexity, which is again in line with data complexity results for basic expressive DLs. We observe that many natural extensions of TGF, including the liberal use of equality, lead to undecidability. We also establish that TGF has the finite model property (providing a tight doubly exponential bound on the model size), whence finite satisfiability coincides with satisfiability.

cs.LO↗

arXiv2025

Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Version)

We study the Guarded Fragment with Regular Guards (RGF), which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many previously-studied extensions of GF, including (conjunctions of) transitive or equivalence guards, transitive or equivalence closure and more. We prove 2EXPTIME-completeness of the satisfiability problem for RGF, showing that RGF is not harder than ICPDL or GF. Shifting to the query entailment problem, we provide undecidability results that significantly strengthen and solidify earlier results along those lines. We conclude by identifying, in a natural sense, the maximal EXPSPACE-complete fragment of RGF.

cs.LO↗

arXiv2023

A Uniform One-Dimensional Fragment with Alternation of Quantifiers

The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment of first-order logic to contexts involving relations of arity greater than two. Quantifiers in this logic are used in blocks, each block consisting only of existential quantifiers or only of universal quantifiers. In this paper we consider the possibility of mixing quantifiers in blocks. We identify a non-trivial variation of the logic with mixed blocks of quantifiers which retains some good properties of the two-variable fragment and of the uniform one-dimensional fragment: it has the finite (exponential) model property and hence decidable, NExpTime-complete satisfiability problem.

cs.LO↗

arXiv2021

Completing the Picture: Complexity of Graded Modal Logics with Converse

A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames have already been established. By "traditional" classes of frames, we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper, we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular, we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.

cs.LO↗

arXiv2021

Finite Model Theory of the Triguarded Fragment and Related Logics

The Triguarded Fragment (TGF) is among the most expressive decidable fragments of first-order logic, subsuming both its two-variable and guarded fragments without equality. We show that the TGF has the finite model property (providing a tight doubly exponential bound on the model size) and hence finite satisfiability coincides with satisfiability known to be N2ExpTime-complete. Using similar constructions, we also establish 2ExpTime-completeness for finite satisfiability of the constant-free (tri)guarded fragment with transitive guards.

cs.LO↗

arXiv2016

Extending Two-Variable Logic on Trees

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

cs.LO↗

arXiv2014

Satisfiability of the Two-Variable Fragment of First-Order Logic over Trees

We consider the satisfiability problem for the two-variable fragment of first-order logic over finite unranked trees. We work with signatures consisting of some unary predicates and the binary navigational predicates child, right sibling, and their respective transitive closures. We prove that the satisfiability problem for the logic containing all these predicates is EXPSPACE-complete. Further, we consider the restriction of the class of structures to singular trees, i.e., we assume that at every node precisely one unary predicate holds. We observe that the full logic and even for unordered trees remain EXPSPACE-complete over finite singular trees, but the complexity decreases for some weaker logics. Namely, the logic with one binary predicate, descendant is NEXPTIME-complete, and its guarded version is PSPACE-complete over finite singular trees, even though both these logics are EXPSPACE-complete over arbitrary finite trees.

cs.LO↗

arXiv2014

Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality

Uniform one-dimensional fragment UF1^= is a formalism obtained from first-order logic by limiting quantification to applications of blocks of existential (universal) quantifiers such that at most one variable remains free in the quantified formula. The fragment is closed under Boolean operations, but additional restrictions (called uniformity conditions) apply to combinations of atomic formulas with two or more variables. The fragment can be seen as a canonical generalization of two-variable logic, defined in order to be able to deal with relations of arbitrary arities. The fragment was introduced recently, and it was shown that the satisfiability problem of the equality-free fragment of UF1^= is decidable. In this article we establish that the satisfiability and finite satisfiability problems of UF1^= are NEXPTIME-complete. We also show that the corresponding problems for the extension of UF1^= with counting quantifiers are undecidable. In addition to decidability questions, we compare the expressivities of UF1^= and two-variable logic with counting quantifiers FOC^2. We show that while the logics are incomparable in general, UF1^= is strictly contained in FOC^2 when attention is restricted to vocabularies with the arity bound two.

math.LO↗