Related papers: Generalized Complexity of ALC Subsumption
Typing of lambda-terms in Elementary and Light Affine Logic (EAL, LAL, resp.) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, resp.) proof-nets admits a guaranteed polynomial…
The number partition problem is a well-known problem, which is one of 21 Karp's NP-complete problems \cite{karp}. The partition function is a boolean function that is equivalent to the number partition problem with number range restricted.…
In this paper we initiate the study of the computational complexity of learning linear temporal logic (LTL) formulas from examples. We construct approximation algorithms for fragments of LTL and prove hardness results; in particular we…
It was shown in Alur et al. [1] that the problem of verifying finite concurrent systems through Linearizability is in EXPSPACE. However, there was still a complexity gap between the easy to obtain PSPACE lower bound and the EXPSPACE upper…
Standpoint linear temporal logic SLTL is a recent formalism able to model possibly conflicting commitments made by distinct agents, taking into account aspects of temporal reasoning. In this paper, we analyse the computational properties of…
We present an almost complete classification of the parameterized complexity of all operator fragments of the satisfiability problem in computation tree logic CTL. The investigated parameterization is the sum of temporal depth and…
Answering a question by Honsell and Plotkin, we show that there are two equations between lambda terms, the so-called subtractive equations, consistent with lambda calculus but not simultaneously satisfied in any partially ordered model…
This paper depicts algorithms for solving the decision Boolean Satisfiability Problem. An extreme problem is formulated to analyze the complexity of algorithms and the complexity for solving it. A novel and easy reformulation as a lottery…
We give the first ExpTime (complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHOQ, which extends the basic description logic ALC with transitive roles, hierarchies of…
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time…
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…
We present a probabilistic extension of the description logic $\mathcal{ALC}$ for reasoning about statistical knowledge. We consider conditional statements over proportions of the domain and are interested in the probabilistic-logical…
We study the logic FO(~), the extension of first-order logic with team semantics by unrestricted Boolean negation. It was recently shown axiomatizable, but otherwise has not yet received much attention in questions of computational…
Description logics (DL) are a family of formal languages for representing and reasoning about structured knowledge in terms of concepts and their relationships. A central reasoning problem in DL is concept subsumption. Although this problem…
We investigate the satisfiability and finite satisfiability problem for probabilistic computation-tree logic (PCTL) where operators are not restricted by any step bounds. We establish decidability for several fragments containing…
The clone of term operations of an algebraic structure consists of all operations that can be expressed by a term in the language of the structure. We consider bounds for the length and the height of the terms expressing these functions,…
We clarify the complexity of answering unions of conjunctive queries over knowledge bases formulated in the description logic $\mathcal S$, the extension of $\mathcal{ALC}$ with transitive roles. Contrary to what existing partial results…
Hybrid logic with binders is an expressive specification language. Its satisfiability problem is undecidable in general. If frames are restricted to N or general linear orders, then satisfiability is known to be decidable, but of…
As fragments of first-order logic, Description logics (DLs) do not provide nonmonotonic features such as defeasible inheritance and default rules. Since many applications would benefit from the availability of such features, several…
We determine all composition-closed equational classes of Boolean functions. These classes provide a natural generalization of clones and iterative algebras: they are closed under composition, permutation and identification…