A Propositional Proof System with Quantification Over Permutations

• Autorzy: Herman G. , Paterson T. , Soltys M.
• Języki publikacji: EN

Abstrakty

EN

We introduce a new propositional proof system, which we call H, that allows quantification over permutations. In H we may write ($ab)a and ("ab)a, which is semantically equivalent to a(a,b)Úa(b,a) and a(a,b)U`a(b,a), respectively. We show that H with cuts restricted to S1 formulas (we denote this system H1) simulates efficiently the Hajós calculus (HC) for constructing graphs which are non-3-colorable. This shows that short proofs over formulas that assert the existence of permutations can capture polynomial time reasoning (as by [9], HC is equivalent in strength to EF, which in turn captures polytime reasoning). We also show that EF simulates efficiently H1*, which is H1 with proofs restricted to being tree-like. In short, we show that [formula]

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 1-2
• Strony: 71--83
• Opis fizyczny: bibliogr. 11 poz.

Twórcy

autor

Herman G.

autor

Paterson T.

autor

Soltys M.

• Department of Computing and Software, McMaster University, Ontario, Canda,

Bibliografia

• [1] Paul Beame and Toniann Pitassi. Propositional proof complexity: Past, present, and future. In Bulletin of the EATCS, volume 65, pages 66-89. Springer-Verlag, June 1998.
• [2] Samuel R. Buss. Some remarks on the lengths of propositional proofs. Archive for Mathematical Logic, 34:377-394, 1995.
• [3] Samuel R. Buss. An introduction to proof theory. In Samuel R. Buss, editor, Handbook of Proof Theory, pages 1-78. North Holland, 1998.
• [4] Stephen Cook and Phuong Nguyen. Foundations of proof complexity: Bounded arithmetic and propositional translations. Available from www.cs.toronto.edu/~sacook/csc2429h/book/, 2006.
• [5] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. JSL, 44:36-50, 1979.
• [6] G. Hajós. ¨Űber eine konstruktion nicht n-färbbarer graphen. Wiss. Zeitschr. Martin Luther Univ. Halle-Wittenberg, 10:116-117, 1961.
• [7] Kazuo Iwama and Toniann Pitassi. Exponential lower bounds for the tree-like Hajós calculus. Inf. Process. Lett., 54(5):289-294, 1995.
• [8] Jan Krajıček. Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge, 1995.
• [9] Toniann Pitassi and Alasdair Urquhart. The complexity of the Hajós calculus. SIAMJ. Disc.Math., 8(3):464-483, August 1995.
• [10] Alasdair Urquhart. The complexity of propositional proofs. Bulletin of Symbolic Logic, 1(4):425-467, 1995.
• [11] Alasdair Urquhart. The symmetry rule in propositional logic. Discrete AppliedMathematics, 96-97:177-193, 1998.