Abstract
It is shown how the schema of equivalence can be used to obtain short proofs of tautologies A, where the depth of proofs is linear in the number of variables in A.
References
Krajíček, J. and P. Pudlák. [1988] The number of proof lines and the size of proofs in first order logic. Arch. Math. Logic, 27, 69–84.
Schütte, K. [1960] Beweistheorie. Springer, Berlin.
Yukami, T. [1984] Some results on speed-up. Ann. Japan Assoc. Philos. Sci., 6, 195–205.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baaz, M., Zach, R. (1994). Short proofs of tautologies using the schema of equivalence. In: Börger, E., Gurevich, Y., Meinke, K. (eds) Computer Science Logic. CSL 1993. Lecture Notes in Computer Science, vol 832. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0049322
Download citation
DOI: https://doi.org/10.1007/BFb0049322
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58277-9
Online ISBN: 978-3-540-48599-5
eBook Packages: Springer Book Archive