THE COMPLEXITY OF THE HAJOS CALCULUS

The Hajo's calculus is a simple, nondeterministic procedure that gener ates the class of non-3-colorable graphs. Mansfield and Welsch posed t he question of whether there exist graphs that require exponential-siz ed Hajos constructions. Unless NP not equal coNP, there must exist gra phs that require exponential-sized constructions, but to date, little progress has been made on this question, despite considerable effort. In this paper, we prove that the Hajos calculus generates polynomial-s ized constructions for all non-3-colorable graphs if and only if exten ded Frege systems are polynomially bounded. Extended Frege systems are a Very powerful family of proof systems for proving tautologies, and proving superpolynomial lower bounds for these systems is a long-stand ing, important problem in logic and complexity theory We also establis h a relationship between a complete subsystem of the Hajos calculus an d bounded-depth Frege systems; this enables us to prove exponential lo wer bounds on this subsystem of the Hajos calculus.