Pebble Games, Proof Complexity, and Time-Space Trade-offs

TL;DR

This paper surveys how pebble games are used in proof complexity to analyze proof space lower bounds and trade-offs between proof size and space, highlighting recent developments and tools.

Contribution

It provides a comprehensive overview of pebbling techniques applied to proof complexity, emphasizing new results on proof space lower bounds and size-space trade-offs.

Findings

Pebbling techniques effectively establish proof space lower bounds.

Trade-offs between proof size and proof space are characterized using pebble games.

Recent research has advanced understanding of proof complexity through pebbling methods.

Abstract

Pebble games were extensively studied in the 1970s and 1980s in a number of different contexts. The last decade has seen a revival of interest in pebble games coming from the field of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on proof space, and establishing size-space trade-offs. This is a survey of research in proof complexity drawing on results and tools from pebbling, with a focus on proof space lower bounds and trade-offs between proof size and proof space.