Abstract
The playground is the projective complex plane. The article shows that usual, naive, lines are not all lines. From naive lines (level 0), Pappus geometry creates new geometric objects (circles or conics) which can also be considered as (level 1) lines, in the sense that they fulfil Pappus axioms for lines. But Pappus theory also applies to these new lines. A formalization of Pappus geometry should enable to automatize these generalizations of lines.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Coxeter, H.: Projective geometry. Springer, Heidelberg (1987)
Henle, M.: Modern Geometries: Non-Euclidean, Projective, and Discrete, 2nd edn. Prentice Hall (2001)
Michelucci, D.: Isometry group, words and proofs of geometric theorems. In: SAC 2008: Proceedings of the 2008 ACM Symposium on Applied Computing, pp. 1821–1825. ACM, New York (2008)
Michelucci, D., Schreck, P.: Incidence constraints: a combinatorial approach. Int. J. Comput. Geometry Appl. 16(5-6), 443–460 (2006)
Richter-Gebert, J., Sturmfels, B., Theobald, T.: First steps in tropical geometry (2003)
Richter-Gebert, J.: Perspectives on Projective Geometry: A Guided Tour Through Real and Complex Geometry. Springer, Heidelberg (2011)
Gao, X.s.: Search methods revisited. In: Mathematics Mechanization and Application, ch. 10, pp. 253–272. Academic Press (2000)
Stahl, S.: The Poincaré Half-Plane. Jones and Bartlett Books in Mathematics (1993)
Wen-Tsün, W.: Mechanical Theorem Proving in Geometries - Basic Principles. Texts and monographs in symbolic computation. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Michelucci, D. (2011). What Is a Line ?. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds) Automated Deduction in Geometry. ADG 2010. Lecture Notes in Computer Science(), vol 6877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25070-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-25070-5_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25069-9
Online ISBN: 978-3-642-25070-5
eBook Packages: Computer ScienceComputer Science (R0)