On Some Proporties of Frege Proofs
Abstract
In [4] a measure s on propositional formula was defined such that for every tautology ϕ "high" value of s(ϕ) requires the large size of proof in the "weak" propositional systems. In this paper it is shown, that there is a tautology ϕ, the measure s(ϕ) of which has exponential dependence on the size of ϕ, but its proof complexity in Frege systems is polynomially bounded.
References
S.R. Buss, Polynomial size proofs of the propositional pigeonhole principle, Journal of Symbolic Logic, 52, 1987, 916-927.
A.A. Chubaryan, On the proof complexity in some system of classical propositional logic, Izvestija NAN Armenii, Mathematika, Vol. 34, N5, 1999, 16-26.
A.A. Chubaryan, On the complexity of proofs in Frege systems, CSIT Conference, Yerevan, 2001, 129-132.
A.A. Chubaryan, Relative efficiency of a proof system in classical propositional logic, Izvestija NAN Armenii, Mathematika, Vol. 37, N5, 2002, 71-84.
S.A. Cook, A.R. Reckhow, The relative efficiency of propositional proof systems, Journal of Symbolic Logic, 1979, 44, 36-50.
E. Mendelson, Introduction to Mathematical Logic, D. Van Nostrand company, INC, Princeton, 1964.
Downloads
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
