Related papers: Complexity of the Ackermann fragment with one lead…

We show that provability in the implicational fragment of relevance logic is complete for doubly exponential time, using reductions to and from coverability in branching vector addition systems.

We consider an extension of the unary negation fragment of first-order logic in which arbitrarily many binary symbols may be required to be interpreted as equivalence relations. We show that this extension has the finite model property.…

We study the exponential time complexity of approximate counting satisfying assignments of CNFs. We reduce the problem to deciding satisfiability of a CNF. Our reduction preserves the number of variables of the input formula and thus also…

We prove that the problem of determining whether a finite logical matrix determines an algebraizable logic is complete for EXPTIME. The same result holds for the classes of order algebraizable, weakly algebraizable, equivalential and…

The constraint satisfaction problem, parameterized by a relational structure, provides a general framework for expressing computational decision problems. Already the restriction to the class of all finite structures forms an interesting…

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified in 1968 by W.V. Quine. We show that the satisfiability problem for this fragment has non-elementary…

This paper shows that the satisfiability problem for probabilistic CTL (PCTL, for short) is undecidable. By a reduction from $1\frac{1}{2}$-player games with PCTL winning objectives, we establish that the PCTL satisfiability problem is…

We classify the complexity of the satisfiability problem for extensions of CTL and UB. The extensions we consider are Boolean combinations of path formulas, fairness properties, past modalities, and forgettable past. Our main result shows…

We systematically investigate the complexity of model checking the existential positive fragment of first-order logic. In particular, for a set of existential positive sentences, we consider model checking where the sentence is restricted…

A worst-case ExpTime tableau-based decision procedure is outlined for the satisfiability problem in $\mathcal{ALCQI}$ w.r.t. general axioms.

We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that…

The standard reasoning problem, concept satisfiability, in the basic description logic ALC is PSPACE-complete, and it is EXPTIME-complete in the presence of unrestricted axioms. Several fragments of ALC, notably logics in the FL, EL, and…

We show that Branching-time temporal logics CTL and CTL*, as well as Alternating-time temporal logics ATL and ATL*, are as semantically expressive in the language with a single propositional variable as they are in the full language, i.e.,…

The finite satisfiability problem for guarded fixpoint logic is decidable and complete for 2ExpTime (resp. ExpTime for formulas of bounded width).

We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the…

We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well…

We show that the consistency problem for Statistical EL ontologies, defined by Pe{\~{n}}aloza and Potyka, is ExpTime-hard. Together with existing ExpTime upper bounds, we conclude ExpTime-completeness of the logic. Our proof goes via a…

We study the finitary satisfiability problem for first order logic with two variables and two binary relations, corresponding to the induced successor relations of two finite linear orders. We show that the problem is decidable in NEXPTIME.

We study the realizability problem for Safety LTL, the syntactic fragment of Linear Temporal Logic capturing safe formulas. We show that the problem is EXP-complete, disproving the existing conjecture of 2EXP-completeness. We achieve this…

In this paper, we determine the complexity of the satisfiability problem for various logics obtained by adding numerical quantifiers, and other constructions, to the traditional syllogistic. In addition, we demonstrate the incompleteness of…