Related papers: The Fluted Fragment with Transitivity
In this paper we consider a fragment of the first-order theory of the real numbers that includes systems of equations of continuous functions in bounded domains, and for which all functions are computable in the sense that it is possible to…
In recent work, comonads and associated structures have been used to analyse a range of important notions in finite model theory, descriptive complexity and combinatorics. We extend this analysis to Hybrid logic, a widely-studied extension…
We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a…
A special case of the satisfiability problem, in which the clauses have a hierarchical structure, is shown to be solvable in linear time, assuming that the clauses have been represented in a convenient way.
We show that descriptive complexity's result extends in High Order Logic to capture the expressivity of Turing Machine which have a finite number of alternation and whose time or space is bounded by a finite tower of exponential. Hence we…
Temporal logics over finite traces have recently seen wide application in a number of areas, from business process modelling, monitoring, and mining to planning and decision making. However, real-life dynamic systems contain a degree of…
We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an $\exists^*\forall^*$ quantifier prefix (over variables, functions…
We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $\Sigma_1$ theory is undecidable (already over two letters). We investigate the decidability…
We show undecidability of the satisfiability problem of what is arguably the simplest non-sub-Boolean modal logic with an implicit notion of binding. This work enriches the series of existing results of undecidability of modal logics with…
Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the domain and interpretations of a structure. We generalize…
We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition…
The logical connectives typically found in programming languages are similar to their mathematical counterparts, yet different due to their short-circuit behaviour -- when evaluating them, the second argument is only evaluated if the first…
We study the computational complexity of model checking and satisfiability problems of polyadic modal logics extended with permutations and Boolean operators on accessibility relations. First, we show that the combined complexity of the…
We introduce the class of synchronous subsequential relations, a subclass of the synchronous relations which embodies some properties of subsequential relations. If we take relations of this class as forming the possible transitions of an…
We describe various strengthenings of the concept of topological transitivity. Especially when one departs from the family of invertible systems, a number of interesting properties arise. We present the architecture of implications among…
We consider a logic used to describe sets of configurations of distributed systems, whose network topologies can be changed at runtime, by reconfiguration programs. The logic uses inductive definitions to describe networks with an unbounded…
The paper considers algorithmic properties of classical and non-classical first-order logics and theories in bounded languages. The main idea is to prove the undecidability of various fragments of classical and non-classical first-order…
Doubts are raised concerning the usual interpretation of the alleged failure, by quantum mechanics, of the distributive law of classical logic. The difficulty raised by incompatible sets of observables is overcome within an epistemic…
We present a completeness result for the implicit fragment of justification stit logic. Although this fragment allows for no strongly complete axiomatization, we show that a restricted form of strong completeness (subsuming weak…
We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is in NP. As an application, we extend the combinatory array logic fragment to handle cardinality constraints.…