enter search term and/or author name
On the Power of Substitution in the Calculus of Structures
Novak Novaković, Lutz Straßburger
Article No.: 19
There are two contributions in this article. First, we give a direct proof of the known fact that Frege systems with substitution can be p-simulated by the calculus of structures (CoS) extended with the substitution rule. This is done without...
Nonelementary Complexities for Branching VASS, MELL, and Extensions
Ranko Lazić, Sylvain Schmitz
Article No.: 20
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 provability...
Bounds for the Quantifier Depth in Finite-Variable Logics: Alternation Hierarchy
Christoph Berkholz, Andreas Krebs, Oleg Verbitsky
Article No.: 21
Given two structures G and H distinguishable in FOk (first-order logic with k variables), let Ak(G, H) denote the minimum alternation depth of a FOk formula...
On the Complexity of Probabilistic Abstract Argumentation Frameworks
Bettina Fazzinga, Sergio Flesca, Francesco Parisi
Article No.: 22
Probabilistic abstract argumentation combines Dung’s abstract argumentation framework with probability theory in order to model uncertainty in argumentation. In this setting, we address the fundamental problem of computing the probability...
The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories
Peter Lefanu Lumsdaine, Michael A. Warren
Article No.: 23
We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive types....
Clique-width is a graph invariant that has been widely studied in combinatorics and computational logic. Computing the clique-width of a graph is an intricate problem, because the exact clique-width is not known even for very small graphs. We...
Many decision problems in formal verification and design can be suitably formulated in game-theoretic terms. This is the case for the model checking of open and closed systems and both controller and reactive synthesis. Interpreted in this...
We address computational complexity writing polymorphic functions between finite types (i.e., types with a finite number of canonical elements), expressing costs in terms of the cardinality of these types. This allows us to...
Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting
Christopher Hampson, Agi Kurucz
Article No.: 27
First-order temporal logics are notorious for their bad computational behavior. It is known that even the two-variable monadic fragment is highly undecidable over various linear timelines, and over branching time even one-variable fragments might...