Abstract
This paper presents an extension of Gentzen's LK, called L PG K, which is suitable for expressing projective geometry and for deducing theorems of plane projective geometry. The properties of this calculus are investigated and the cut elimination theorem for L PG K is proven. A formulization of sketches is presented and the equivalence between sketches and formal proofs is demonstrated.
Supported by the Austrian Research Fund (FWF Projekt P11934-MAT)
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Matthias Baaz. Generalization of proofs and term complexity. In Logic Colloquium '94, Main Lecture, Clermont, France, 1994. Unpublished manuscript.
H. S. M. Coxeter. Projective Geometry. Springer-Verlag, 1994.
David Hilbert. Grundlagen der Geometric. B. G. Teubner, 1899.
J. KrajĂÄŤek and P. Pudlák. The number of proof lines and the size of proofs in first order logic. Arch. Math. Logic, pages 69–84, 1988.
Norbert Preining. Sketch-as-proof, a proof-theoretic analysis of axiomatic projective geometry. Master's thesis, University of Technology, Vienna, Austria, 1996. ftp://ftp.logic.tuvien.ac.at/pub/preining/sketch-as-proof.ps.
Gaisi Takeuti. Proof Theory. North Holland, 1987.
Alfred Tarski. On essential undecidability. Journal of Symbolic Logic, 14:75–78, 1949.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Preining, N. (1997). Sketch-as-proof. In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1997. Lecture Notes in Computer Science, vol 1289. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63385-5_49
Download citation
DOI: https://doi.org/10.1007/3-540-63385-5_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63385-3
Online ISBN: 978-3-540-69806-7
eBook Packages: Springer Book Archive