Seminario Interdipartimentale di Algoritmica  

Monday, March 7, 2005, 12:00 noon
Theorem Provers by Pebbling Games
Nicola Galesi
Università di Roma "La Sapienza"

DI - Department of Computer Science
Seminar Room, third floor

Abstract:

We do not expect to find a resolution theorem prover with polynomial running time unless some unexpected complexity result would hold. Hence in looking for such algorithms it seems natural at least to require time-efficiency in the size of the shortest proof of the theorem we want to generate a proof. When efficiency means polynomially bounded we say that resolution is automatizable. Ben-Sasson and Wigderson (BSW) presented a very simple algorithm that achieved a sub-exponential automatizability for resolution. Using the simple property (LOP) that every finite linearly ordered set has a minimal element, we proved that the sub-exponential bound is the best possible for their algorithm. Surprising enough, LOP is essentially the only example so far known to prove that. Moreover it appears to be a sort of "black beast" for many theorem provers, in particular for the most used in applications. There are short resolution refutations of LOP, but many algorithms fail to generate them efficiently. In the talk I'll present a characterization of resolution through pebbling games. Using games we devise a new algorithm to generate refutations which, from the automatizability point of view, is as good as the BSW algorithm, and that moreover generates polynomially short refutations of LOP formulae when its variables respect any given order.

The content of the talk is part of a joint work with Neil Thapen (Oxford University).