# Time and Space in Proof Complexity

Report ID:
TR-998-16
Authors:
Date:
December 7, 2016
Pages:
117
[PDF]

#### Abstract:

In this thesis we explore the limitations of efficient computation by way of the complexity
of proofs.
One of the goals of theoretical computer science is to understand algorithms broadly
– to identify meta-algorithms that may be useful in a variety of cases, understand how
they work, when they work well, and when they don’t.
For several important groups of algorithms, there is a relatively simple mathematical
proof that the algorithm is correct for every input. Moreover, when the algorithm is run
on any particular input, this proof specializes to produce a very simple combinatorial
proof of the correct answer for that input. A simple example is a linear program, which
may find an optimal point and give a dual solution proving the optimality, or a graph
search algorithm which may fail to find a path between two points and yield a cut
Often times, self-contained proofs that the answer to some query is yes or no are just
as important as the answer itself. When the algorithm is meant to identify problems in
some system, or opportunities, the proof may actually represent actionable information
in some domain. A good example is when a SAT solver is used to validate a system that
is being designed. When the validation fails, the proof indicates where the problem is
with the current design.
Proof complexity attempts to place limits on how efficient such algorithms can be
by showing that these proofs must sometimes be very complex, growing rapidly as the
problem scales up. More broadly, proof complexity attempts to understand the proving
power of traditional formal systems for logic, and to corroborate hypotheses like P !=
NP.
We develop novel combinatorial techniques for studying proof complexity in several
well-studied proof systems. We give substantial quantitative improvements on existing
results, and also, develop a new method that allows us to study the time and space
needed for a proof simultaneously and prove “tradeoff” lower bounds. We show that
small reductions in space can sometimes lead to large increases in time, even in situations
where the algorithm has large amounts of space to work with. Previously no such
results were known in that situation.