Switch to: References

Add citations

You must login to add citations.
  1. Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
    A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1) Feasible (...)
    Direct download (11 more)  
    Export citation  
    Bookmark   13 citations  
  • Upper Bounds on Complexity of Frege Proofs with Limited Use of Certain Schemata.Pavel Naumov - 2005 - Archive for Mathematical Logic 45 (4):431-446.
    The paper considers a commonly used axiomatization of the classical propositional logic and studies how different axiom schemata in this system contribute to proof complexity of the logic. The existence of a polynomial bound on proof complexity of every statement provable in this logic is a well-known open question.The axiomatization consists of three schemata. We show that any statement provable using unrestricted number of axioms from the first of the three schemata and polynomially-bounded in size set of axioms from the (...)
    Direct download (4 more)  
    Export citation  
  • Resolution Over Linear Equations and Multilinear Proofs.Ran Raz & Iddo Tzameret - 2008 - Annals of Pure and Applied Logic 155 (3):194-224.
    We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead of clauses. We demonstrate polynomial-size refutations for hard tautologies like the pigeonhole principle, Tseitin graph tautologies and the clique-coloring tautologies in these proof systems. Using interpolation we establish an exponential-size lower bound on refutations in a certain, considerably strong, fragment of resolution over linear equations, as well as a general polynomial upper bound on interpolants (...)
    Direct download (7 more)  
    Export citation  
    Bookmark   1 citation