A Simulation of Natural Deduction and Gentzen Sequent Calculus
DOI:
https://doi.org/10.12775/LLP.2017.009Keywords
speedup, natural deduction, Gentzen-style calculi, simulation, proof systemAbstract
We consider four natural deduction systems: Fitch-style systems, Gentzen-style systems (in the form of dags), general deduction Frege systems and nested deduction Frege systems, as well as dag-like Gentzen-style sequent calculi. All these calculi soundly and completely formalize classical propositional logic.
We show that general deduction Frege systems and Gentzen-style natural calculi provide at most quadratic speedup over nested deduction Frege systems and Fitch-style natural calculi and at most cubic speedup over Gentzen-style sequent calculi.
References
Bonet, M.L., and S.R. Buss, “The deduction rule and linear and nearlinear proof simulations”, The Journal of Symbolic Logic 58, 2 (1993): 688–709. DOI: 10.2307/2275228
Buss, S.R. (ed.), Handbook of Proof Theory, volume 137 of Studies in Logic and Foundations of Mathematic, Elsevier Science, Amsterdam, 1st edition, 1998.
Cook, S.A., and P. Nguyen, Logical Foundations of Proof Complexity, Cambridge University Press, Cambridge, 2010.
Cook, S.A., and R.A. Reckhow, “The relative efficiency of propositional proof systems”, The Journal of Symbolic Logic 44, 1 (1979): 36–50. DOI: 10.2307/2273702
D’Agostino, M., Investigations into the Complexity of Some Propositional Calculi, Oxford University Computing Laboratory, Oxford, 1990.
Finger, M., “Dag sequent proofs with a substitution rule”, pages 671–686 in We Will Show Them: Essays in Honor of Dov Gabbay’s 60th Birthday, London, Kings College Publications, 2005.
Fitch, F.B., Symbolic Logic: An Introduction, The Ronald Press Company, N.Y., 1952.
Gentzen, G., “Untersuchungen über das logische Schließen I”, Mathematische Zeitschrift 39 (1935): 176–210. DOI: 10.1007/BF01201353
Jaśkowski, S., “On the rules of supposition in formal logic”, Studia Logica 1 (1934).
Krajìček, J., “On the number of steps in proofs”, Annals of Pure and Applied Logics 41 (1989): 153–178.
Papadimitriou, C.H., Computational Complexity, Addison-Wesley Publishing Company, Inc., NY, 1995.
Pelletier, F.J., “A brief history of natural deduction”, History and Philosophy of Logic 20 (1999): 1–31. DOI: 10.1080/014453499298165
Reckhow, R.A., “On the lengths of proofs in the propositional calculus”, PhD thesis, University of Toronto, 1976.
Smullyan, R.M., First-Order Logic, Dover Publications, Inc., N.Y., 1995.
Tseitin, G.S., On the Complexity of Derivation in Propositional Calculus, pages 466–483, Springer-Verlag, NY, 1983.
Urquhart, A., “The complexity of gentzen systems for propositional logic”, Theoretical Computer Science 66, 1 (1989): 87–97. DOI: 10.1016/0304-3975(89)90147-3
Urquhart, A., “The relative complexity of resolution and cut-free Gentzen systems”, Annals of Mathematics and Artificial Intelligence 6, 1–3 (1992): 157–168. DOI: 10.1007/BF01531026
Urquhart, A., “The complexity of propositional proofs”, The Bulletin of Symbolic Logic 1, 4 (1995): 425–467.
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 882
Number of citations: 2
