All reports by Author Nicola Galesi:

__
TR14-146
| 6th November 2014
__

Ilario Bonacina, Nicola Galesi, Tony Huynh, Paul Wollan#### Space proof complexity for random $3$-CNFs via a $(2-\epsilon)$-Hall's Theorem

__
TR14-138
| 29th October 2014
__

Nicola Galesi, Pavel Pudlak, Neil Thapen#### The space complexity of cutting planes refutations

__
TR14-038
| 24th March 2014
__

Ilario Bonacina, Nicola Galesi, Neil Thapen#### Total space in resolution

Revisions: 1

__
TR12-161
| 20th November 2012
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria#### A Characterization of Tree-Like Resolution Size

__
TR12-119
| 24th September 2012
__

Ilario Bonacina, Nicola Galesi#### Pseudo-partitions, Transversality and Locality: A Combinatorial Characterization for the Space Measure in Algebraic Proof Systems

__
TR10-198
| 13th December 2010
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander Razborov#### Parameterized Bounded-Depth Frege is Not Optimal

__
TR10-153
| 7th October 2010
__

Lorenzo Carlucci, Nicola Galesi, Massimo Lauria#### Paris-Harrington tautologies

Revisions: 2

__
TR10-081
| 10th May 2010
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria#### A Lower Bound for the Pigeonhole Principle in Tree-like Resolution by Asymmetric Prover-Delayer Games

__
TR10-059
| 8th April 2010
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria#### Hardness of Parameterized Resolution

__
TR09-035
| 26th March 2009
__

Nicola Galesi, Massimo Lauria#### On the Automatizability of Polynomial Calculus

__
TR07-041
| 20th April 2007
__

Nicola Galesi, Massimo Lauria#### Extending Polynomial Calculus to $k$-DNF Resolution

Revisions: 1

__
TR04-112
| 26th November 2004
__

Neil Thapen, Nicola Galesi#### Resolution and pebbling games

__
TR01-031
| 5th April 2001
__

Eli Ben-Sasson, Nicola Galesi#### Space Complexity of Random Formulae in Resolution

__
TR00-087
| 14th November 2000
__

Albert Atserias, Nicola Galesi, Pavel Pudlak#### Monotone simulations of nonmonotone propositional proofs

__
TR00-008
| 20th January 2000
__

Albert Atserias, Nicola Galesi, Ricard GavaldÃ#### Monotone Proofs of the Pigeon Hole Principle

Ilario Bonacina, Nicola Galesi, Tony Huynh, Paul Wollan

We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. No lower bound for refuting any family of $3$-CNFs was previously known for the total space in resolution or for the monomial space in algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a ... more >>>

Nicola Galesi, Pavel Pudlak, Neil Thapen

We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of inequalities that need to be kept on a blackboard while verifying it. We show that any ... more >>>

Ilario Bonacina, Nicola Galesi, Neil Thapen

We show $\Omega(n^2)$ lower bounds on the total space used in resolution refutations of random $k$-CNFs over $n$ variables, and of the graph pigeonhole principle and the bit pigeonhole principle for $n$ holes. This answers the long-standing open problem of whether there are families of $k$-CNF formulas of size $O(n)$ ... more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

We explain an asymmetric Prover-Delayer game which precisely characterizes proof size in tree-like Resolution. This game was previously described in a parameterized complexity context to show lower bounds for parameterized formulas and for the classical pigeonhole principle. The main point of this note is to show that the asymmetric game ... more >>>

Ilario Bonacina, Nicola Galesi

We devise a new combinatorial characterization for proving space lower bounds in algebraic systems like Polynomial Calculus (Pc) and Polynomial Calculus with Resolution (Pcr). Our method can be thought as a Spoiler-Duplicator game, which is capturing boolean reasoning on polynomials instead that clauses as in the case of Resolution. Hence, ... more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander Razborov

A general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that framework the parameterized version of any proof system is not fpt-bounded for some technical reasons, but we remark that this question becomes much more interesting if we restrict ourselves to those parameterized contradictions ... more >>>

Lorenzo Carlucci, Nicola Galesi, Massimo Lauria

We initiate the study of the proof complexity of propositional encoding of (weak cases of) concrete independence results. In particular we study the proof complexity of Paris-Harrington's Large Ramsey Theorem. We prove a conditional lower bound in Resolution and a quasipolynomial upper bound in bounded-depth Frege.

more >>>Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

In this note we show that the asymmetric Prover-Delayer game developed by Beyersdorff, Galesi, and Lauria (ECCC TR10-059) for Parameterized Resolution is also applicable to other tree-like proof systems. In particular, we use this asymmetric Prover-Delayer game to show a lower bound of the form $2^{\Omega(n\log n)}$ for the pigeonhole ... more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles.

We broadly investigate Parameterized Resolution obtaining the following ...
more >>>

Nicola Galesi, Massimo Lauria

We prove that Polynomial Calculus and Polynomial Calculus with Resolution are not automatizable, unless W[P]-hard problems are fixed parameter tractable by one-side error randomized algorithms. This extends to Polynomial Calculus the analogous result obtained for Resolution by Alekhnovich and Razborov (SIAM J. Computing, 38(4), 2008).

more >>>Nicola Galesi, Massimo Lauria

We introduce an algebraic proof system Pcrk, which combines together {\em Polynomial Calculus} (Pc) and {\em $k$-DNF Resolution} (Resk).

This is a natural generalization to Resk of the well-known {\em Polynomial Calculus with Resolution} (Pcr) system which combines together Pc and Resolution.

We study the complexity of proofs in such ... more >>>

Neil Thapen, Nicola Galesi

We define a collection of Prover-Delayer games that characterize certain subsystems of resolution. This allows us to give some natural criteria which guarantee lower bounds on the resolution width of a formula, and to extend these results to formulas of unbounded initial width.

We also use games to give upper ... more >>>

Eli Ben-Sasson, Nicola Galesi

We study the space complexity of refuting unsatisfiable random $k$-CNFs in

the Resolution proof system. We prove that for any large enough $\Delta$,

with high probability a random $k$-CNF over $n$ variables and $\Delta n$

clauses requires resolution clause space of

$\Omega(n \cdot \Delta^{-\frac{1+\epsilon}{k-2-\epsilon}})$,

for any $0<\epsilon<1/2$. For constant $\Delta$, ...
more >>>

Albert Atserias, Nicola Galesi, Pavel Pudlak

We show that an LK proof of size $m$ of a monotone sequent (a sequent

that contains only formulas in the basis $\wedge,\vee$) can be turned

into a proof containing only monotone formulas of size $m^{O(\log m)}$

and with the number of proof lines polynomial in $m$. Also we show

... more >>>Albert Atserias, Nicola Galesi, Ricard GavaldÃ

We study the complexity of proving the Pigeon Hole

Principle (PHP) in a monotone variant of the Gentzen Calculus, also

known as Geometric Logic. We show that the standard encoding

of the PHP as a monotone sequent admits quasipolynomial-size proofs

in this system. This result is a consequence of ...
more >>>