Search ACM DL

Search Issue

enter search term and/or author name

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