Abstract
We investigate the complexity of proofs in Frege (F), Substitution Frege (sF) and Renaming Frege (rF) systems. Starting from a recent work of Urquhart and using Kolmogorov Complexity we give a more general framework to obtain superlogarithmic lower bounds for the number of lines in both tree-like and dag-like sF. We show the previous known lower bound, extend it to the tree-like case and, for another class of tautologies, we give new lower bounds that in the dag-like case slightly improve the previous one. Also we show optimality of Urquhart's lower bounds giving optimal proofs. Finally we give the following two simulation results: (1) tree-like sF p-simulates dag-like sF; (2) Tree-like F p-simulates tree-like rF.
Research partly supported by NSF grant number CCR-9403447.
Supported by European Community grant under the project Training and Mobility of Researchers.
Preview
Unable to display preview. Download preview PDF.
References
R. A. Baeza-Yates, R. Gavaldá, G. Navarro. Bounding the Expected Length of Longest Common Subsequences and Forest. Invited talk at the Third South American Workshop on String Processing (WSP'96), Recife (Brazil), Aug. 8–9 1996.
M. Bonet. Number of symbols in Frege proofs with and without the deduction rule. In Arithmetic, proof theory and computational complexity. Oxford University Press Eds. P. Clote and J. Krajiček-1992.
M. Bonet, S. Buss. The deduction rule and linear and near-linear proof simulations. Journal of Symbol Logic, 58 (1993) pp. 688–709.
S. Buss. Some remarks on length of propositional proofs. Archive for Mathematical Logic. 34 (1995) pp. 377–394.
S. Buss, Lectures on proof theory. TR SOCS-96.1 School of C.S.-Mc Gill University 1996.
S. Cook, R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44 (1979) pp. 36–50.
J. H. Gallier. Logic for Computer Science-Foundations of Automatic Theorem Proving. J. Wiley & Sons. 1987
J. R. Hindley, D. Meredith. Principal type schemes and condensed detachment. Journal of Symbolic Logic, 55 (1990) pp. 90–105.
K. Iwana, T. Pitassi. Exponential Lower bounds for the tree-like Hajós Calculus. Manuscript1997.
J. Krajiček. Speed-up for propositional Frege systems via generalizations of proofs. Commentationes Mathernaticae Universiatatis Carolinae, 30 (1989) pp. 137–140.
J. Krajiček. On the number of steps in proof. Annals of Pure and Applied Logic, 41 (1989) pp. 153–178.
J. Krajiček, P. Pudlák. Propositional proof systems, the consistency of first order theories and the complexity of computation. Journal of Symbolic Logic, 54 (1989) pp. 1063–1079ia.
M.Li, P. Vitanyi. An Introduction to Kolmogorov Complexity and its Application. Springer-Verlag 1993.
V.P. Orevkov. Reconstruction of a proof from its scheme. Soviet Mathematics Doklady 35 (1987) pp. 326–329.
V.P. Orevkov. On lower bounds on the lengths of proofs in propositional logic. (In Russian), in Proc, of All Union Conf. Metody Matem. v Problemach iskusstvennogo intellekta i sistematicheskoje programmirovanie, Vilnius, Vol I. 1980. pp. 142–144.
R. Parikh Some results on the length of proofs. Trans. A.M.S., 177 (1973) pp. 29–36.
A. N. Prior. Formal Logic. Oxford, second edition, 1960.
P. Pudlak, S. Buss. How to he without being (easily) convicted and the length of proofs in propositional calculus. 8th Workshop on CSL, Kazimierz, Poland, September 1994, Springer Verlag LNCS n.995, 1995, pp. 151–162.
A. Urquhart. The number of lines in Frege proof with substitution. Archive for Mathematical Logic. To appear.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonet, M.L., Galesi, N. (1998). Linear lower bounds and simulations in frege systems with substitutions. In: Nielsen, M., Thomas, W. (eds) Computer Science Logic. CSL 1997. Lecture Notes in Computer Science, vol 1414. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028010
Download citation
DOI: https://doi.org/10.1007/BFb0028010
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64570-2
Online ISBN: 978-3-540-69353-6
eBook Packages: Springer Book Archive