enter search term and/or author name
Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations
Russell Impagliazzo, Nathan Segerlind
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
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
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
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
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
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
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...