Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > KEYWORD > AUTOMATIZABILITY:
Reports tagged with automatizability:
TR04-112 | 26th November 2004
Neil Thapen, Nicola Galesi

Resolution and pebbling games

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 >>>


TR10-197 | 14th December 2010
Albert Atserias, Elitza Maneva

Mean-payoff games and propositional proofs

We associate a CNF-formula to every instance of the mean-payoff game problem in such a way that if the value of the game is non-negative the formula is satisfiable, and if the value of the game is negative the formula has a polynomial-size refutation in $\Sigma_2$-Frege (i.e.~DNF-resolution). This reduces mean-payoff ... more >>>


TR13-070 | 4th May 2013
Iddo Tzameret

On Sparser Random 3SAT Refutation Algorithms and Feasible Interpolation

Revisions: 1

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 >>>


TR13-094 | 13th June 2013
Brendan Juba

On Non-automatizability in PAC-Semantics

We consider the proof search ("automatizability") problem for integrated learning and reasoning, a problem modeling certain kinds of data mining and common sense reasoning (Juba, 2013a). In such a problem, the approximate validity (i.e., under Valiant’s PAC-Semantics (Valiant, 2000)) of an input query formula over a background probability distribution is ... more >>>




ISSN 1433-8092 | Imprint