ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 7 Issue 2, April 2006

Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations
Russell Impagliazzo, Nathan Segerlind
Pages: 199-218
DOI: 10.1145/1131313.1131314
We show that constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo m. Central to this is a new definition of reducibility from propositional formulas to systems of...

Optimizing optimal reduction: A type inference algorithm for elementary affine logic
Paolo Coppola, Simone Martini
Pages: 219-260
DOI: 10.1145/1131313.1131315
We propose a type inference algorithm for lambda terms in elementary affine logic (EAL). The algorithm decorates the syntax tree of a simple typed lambda term and collects a set of linear constraints. The result is a parametric elementary type that...

Why are there so many loop formulas?
Vladimir Lifschitz, Alexander Razborov
Pages: 261-268
DOI: 10.1145/1131313.1131316
A theorem by Lin and Zhao shows how to turn any nondisjunctive logic program, understood in accordance with the answer set semantics, into an equivalent set of propositional formulas. The set of formulas generated by this process can be significantly...

Decidability results for sets with atoms
Agostino Dovier, Andrea Formisano, Eugenio G. Omodeo
Pages: 269-301
DOI: 10.1145/1131313.1131317
Formal set theory is traditionally concerned with pure sets; consequently, the satisfiability problem for fragments of set theory was most often addressed (and in many cases positively solved) in the pure framework. In practical applications,...

Propositional computability logic I
Giorgi Japaridze
Pages: 302-330
DOI: 10.1145/1131313.1131318
In the same sense as classical logic is a formal theory of truth, the recently initiated approach called computability logic is a formal theory of computability. It understands (interactive) computational problems as games played by a machine...

Propositional computability logic II
Giorgi Japaridze
Pages: 331-362
DOI: 10.1145/1131313.1131319
Computability logic is a formal theory of computational tasks and resources. Its formulas represent interactive computational problems, logical operators stand for operations on computational problems, and validity of a formula is understood as its...

Ordinary interactive small-step algorithms, I
Andreas Blass, Yuri Gurevich
Pages: 363-419
DOI: 10.1145/1131313.1131320
This is the first in a series of articles extending the abstract state machine thesis---that arbitrary algorithms are behaviorally equivalent to abstract state machines---to algorithms that can interact with their environments during a step rather...