A Conditional Superpolynomial Lower Bound for Extended Resolution

详细信息    查看全文

• 作者：Olga Tveretina (18)
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2013
• 出版时间：2013
• 年：2013
• 卷：7810
• 期：1
• 页码：570-578
• 全文大小：206KB
• 参考文献：1. Alon, N., Boppana, R.: The monotone circuit complexity of boolean functions. Combinatorica聽7(1), 1鈥?2 (1987) CrossRef
  2. Bonet, M.L., Pitassi, T., Raz, R.: No feasible interpolation for TC⁰-Frege proofs. In: FOCS, pp. 254鈥?63 (1997)
  3. Cook, S.: Feasibly constructive proofs and the propositional calculus (preliminary version). In: Proceedings of the 7th Annual ACM Symposium on Theory of Computing (STOC), pp. 83鈥?7 (1975)
  4. Cook, S.: A short proof of the pigeon hole principle using extended resolution. ACM SIGACT News聽8(4), 28鈥?2 (1976) CrossRef
  5. Cook, S., Reckhow, R.: On the lengths of proofs in the propositional calculus (preliminary version). In: STOC, pp. 135鈥?48 (1974)
  6. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. Journal of Symbolic Logic聽22(3), 250鈥?68 (1957) CrossRef
  7. Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic聽22(3), 269鈥?85 (1957) CrossRef
  8. Diffie, W., Hellman, M.: New directions in cryptography. IEEE Transactions on Information Theory聽22(6), 644鈥?54 (1976) CrossRef
  9. Kraj铆cek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic聽62(2), 457鈥?86 (1997) CrossRef
  10. Mundici, D.: A lower bound for the complexity of Craig鈥檚 interpolants in sentential logic. Archiv. Math. Logik聽23, 27鈥?6 (1983) CrossRef
  11. Razborov, A.A.: Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izv. RAN. Ser. Mat.聽59, 201鈥?24 (1995)
  12. Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM (JACM)聽12(1), 23鈥?1 (1965) CrossRef
  13. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Leningrad Seminar on Mathematical Logic (1970)
  14. Yao, A.C.: Some complexity questions related to distributive computing (preliminary report). In: STOC, pp. 209鈥?13 (1979)
  
• 作者单位：Olga Tveretina (18)
  
  18. School of Computer Science, University of Hertfordshire, UK
  
• ISSN：1611-3349

文摘

Extended resolution is a propositional proof system that simulates polynomially very powerful proof systems such as Frege systems and extended Frege systems. Feasible interpolation has been one of the most promising approaches for proving lower bounds for propositional proof systems and for bounded arithmetic. We show that an extended resolution refutation of an unsatisfiable CNF representing the clique-graph colouring principle admits feasible interpolation. It gives us a conditional result: If there is a superpolynomial lower bound on the non-monotone circuit size for this class of formulas then extended resolution has a superpolynomial lower bound.