ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 16 Issue 3, July 2015

On the Power of Substitution in the Calculus of Structures
Novak Novaković, Lutz Straßburger
Article No.: 19
DOI: 10.1145/2701424

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
DOI: 10.1145/2733375

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
DOI: 10.1145/2732409

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
DOI: 10.1145/2749463

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
DOI: 10.1145/2754931

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.

...

A SAT Approach to Clique-Width
Marijn J. H. Heule, Stefan Szeider
Article No.: 24
DOI: 10.1145/2736696

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...

Reasoning About Substructures and Games
Massimo Benerecetti, Fabio Mogavero, Aniello Murano
Article No.: 25
DOI: 10.1145/2757286

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...

Computational Complexity Via Finite Types
Andrea Asperti
Article No.: 26
DOI: 10.1145/2764906

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
DOI: 10.1145/2757285

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...