Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 11 Issue 4, July 2010

CSL 2008 special issue
Michael Kaminski, Simone Martini
Article No.: 21
DOI: 10.1145/1805950.1805951

A tight Karp-Lipton collapse result in bounded arithmetic
Olaf Beyersdorff, Sebastian Müller
Article No.: 22
DOI: 10.1145/1805950.1805952

Cook and Krajíček have recently obtained the following Karp-Lipton collapse result in bounded arithmetic: if the theory PV proves NP⊆ P/poly, then the polynomial hierarchy collapses to the Boolean hierarchy, and...

Quantitative languages
Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger
Article No.: 23
DOI: 10.1145/1805950.1805953

Quantitative generalizations of classical languages, which assign to each word a real number instead of a Boolean value, have applications in modeling resource-constrained computation. We use weighted automata (finite automata with transition...

Nonuniform Boolean constraint satisfaction problems with cardinality constraint
Nadia Creignou, Henning Schnoor, Ilka Schnoor
Article No.: 24
DOI: 10.1145/1805950.1805954

We study the computational complexity of Boolean constraint satisfaction problems with cardinality constraint. A Galois connection between clones and coclones has received a lot of attention in the context of complexity considerations for...

On isomorphisms of intersection types
Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
Article No.: 25
DOI: 10.1145/1805950.1805955

The study of type isomorphisms for different λ-calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the...

Pure pointer programs with iteration
Martin Hofmann, Ulrich Schöpp
Article No.: 26
DOI: 10.1145/1805950.1805956

Many logspace algorithms are naturally described as programs that operate on a structured input (e.g., a graph), that store in memory only a constant number of pointers (e.g., to graph nodes) and that do not use pointer arithmetic. Such...

Superposition for fixed domains
Matthias Horbach, Christoph Weidenbach
Article No.: 27
DOI: 10.1145/1805950.1805957

Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the theory....

Typing streams in the Λμ-calculus
Alexis Saurin
Article No.: 28
DOI: 10.1145/1805950.1805958

Λμ-calculus is a Böhm-complete extension of Parigot's Λμ-calculus closely related with delimited control in functional programming. In this article, we investigate the meta-theory of untyped Λμ-calculus by...

Erratum for “What causes a system to satisfy a specification?”
Hana Chockler, Joseph Y. Halpern, Orna Kupferman
Article No.: 29
DOI: 10.1145/1805950.1805959