All reports by Author Iddo Tzameret:

__
TR18-184
| 5th November 2018
__

Iddo Tzameret, Stephen Cook#### Uniform, Integral and Feasible Proofs for the Determinant Identities

__
TR18-117
| 23rd June 2018
__

Fedor Part, Iddo Tzameret#### Resolution with Counting: Lower Bounds over Different Moduli

Revisions: 1

__
TR16-101
| 1st July 2016
__

Toniann Pitassi, Iddo Tzameret#### Algebraic Proof Complexity: Progress, Frontiers and Challenges

__
TR16-098
| 16th June 2016
__

Michael Forbes, Amir Shpilka, Iddo Tzameret, Avi Wigderson#### Proof Complexity Lower Bounds from Algebraic Circuit Complexity

__
TR15-134
| 19th August 2015
__

Fu Li, Iddo Tzameret, Zhengyu Wang#### Characterizing Propositional Proofs as Non-Commutative Formulas

__
TR13-185
| 24th December 2013
__

Fu Li, Iddo Tzameret#### Generating Matrix Identities and Proof Complexity Lower Bounds

Revisions: 3

__
TR13-070
| 4th May 2013
__

Iddo Tzameret#### On Sparser Random 3SAT Refutation Algorithms and Feasible Interpolation

Revisions: 1

__
TR12-028
| 30th March 2012
__

Eric Allender, George Davie, Luke Friedman, Samuel Hopkins, Iddo Tzameret#### Kolmogorov Complexity, Circuits, and the Strength of Formal Theories of Arithmetic

Revisions: 1

__
TR11-174
| 30th December 2011
__

Pavel Hrubes, Iddo Tzameret#### Short Proofs for the Determinant Identities

Revisions: 1

__
TR11-006
| 20th January 2011
__

Sebastian MÃ¼ller, Iddo Tzameret#### Average-Case Separation in Proof Complexity: Short Propositional Refutations for Random 3CNF Formulas

Revisions: 1

__
TR10-097
| 16th June 2010
__

Iddo Tzameret#### Algebraic Proofs over Noncommutative Formulas

Revisions: 1

__
TR07-078
| 11th August 2007
__

Ran Raz, Iddo Tzameret#### Resolution over Linear Equations and Multilinear Proofs

__
TR06-001
| 1st January 2006
__

Ran Raz, Iddo Tzameret#### The Strength of Multilinear Proofs

Iddo Tzameret, Stephen Cook

Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over $GF(2)$ in Hrubes-Tzameret [SICOMP'15]. Specifically, we show that the multiplicativity of the determinant function and the ... more >>>

Fedor Part, Iddo Tzameret

Resolution over linear equations (introduced in [RT08]) emerged recently as an important object of study. This refutation system, denoted Res(lin$_R$), operates with disjunction of linear equations over a ring $R$. On the one hand, the system captures a natural ``minimal'' extension of resolution in which efficient counting can be achieved; ... more >>>

Toniann Pitassi, Iddo Tzameret

We survey recent progress in the proof complexity of strong proof systems and its connection to algebraic circuit complexity, showing how the synergy between the two gives rise to new approaches to fundamental open questions, solutions to old problems, and new directions of research. In particular, we focus on tight ... more >>>

Michael Forbes, Amir Shpilka, Iddo Tzameret, Avi Wigderson

We give upper and lower bounds on the power of subsystems of the Ideal Proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi, where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the ...
more >>>

Fu Li, Iddo Tzameret, Zhengyu Wang

Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional-calculus (i.e., Frege) proof is any proof starting from a set of axioms and deriving new Boolean formulas using a fixed set of sound derivation rules. Establishing any super-polynomial size lower bound on Frege proofs (in terms of the ... more >>>

Fu Li, Iddo Tzameret

Motivated by the fundamental lower bounds questions in proof complexity, we investigate the complexity of generating identities of matrix rings, and related problems. Specifically, for a field $\mathbb{F}$ let $A$ be a non-commutative (associative) $\mathbb{F}$-algebra (e.g., the algebra Mat$_d(\mathbb{F})\;$ of $d\times d$ matrices over $\mathbb{F}$). We say that a non-commutative ... more >>>

Iddo Tzameret

We formalize a combinatorial principle, called the 3XOR principle, due to Feige, Kim and Ofek (2006), as a family of unsatisfiable propositional formulas for which refutations of small size in any propositional proof system that possesses the feasible interpolation property imply an efficient *deterministic* refutation algorithm for random 3SAT with ... more >>>

Eric Allender, George Davie, Luke Friedman, Samuel Hopkins, Iddo Tzameret

Can complexity classes be characterized in terms of efficient reducibility to the (undecidable) set of Kolmogorov-random strings? Although this might seem improbable, a series of papers has recently provided evidence that this may be the case. In particular, it is known that there is a class of problems $C$ defined ... more >>>

Pavel Hrubes, Iddo Tzameret

We study arithmetic proof systems $\mathbb{P}_c(\mathbb{F})$ and $\mathbb{P}_f(\mathbb{F})$ operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field $\mathbb{F}$. We establish a series of structural theorems about these proof systems, the main one stating that $\mathbb{P}_c(\mathbb{F})$ proofs can be balanced: if a polynomial identity of ... more >>>

Sebastian MÃ¼ller, Iddo Tzameret

Separating different propositional proof systems---that is, demonstrating that one proof system cannot efficiently simulate another proof system---is one of the main goals of proof complexity. Nevertheless, all known separation results between non-abstract proof systems are for specific families of hard tautologies: for what we know, in the average case all ... more >>>

Iddo Tzameret

We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege--yielding a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic analogue of Frege proofs, different from that given in Buss ... more >>>

Ran Raz, Iddo Tzameret

We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead of clauses. We demonstrate polynomial-size refutations for hard tautologies like the pigeonhole principle, Tseitin graph tautologies and the clique-coloring tautologies in these proof systems. ... more >>>

Ran Raz, Iddo Tzameret

We introduce an algebraic proof system that manipulates multilinear arithmetic formulas. We show that this proof system is fairly strong, even when restricted to multilinear arithmetic formulas of a very small depth. Specifically, we show the following:

1. Algebraic proofs manipulating depth 2 multilinear arithmetic formulas polynomially simulate Resolution, Polynomial ... more >>>