Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach

Pascal Schreck
(ICube, UMR 7357 CNRS \\ Université de Strasbourg, France)
Nicolas Magaud
(ICube, UMR 7357 CNRS \\ Université de Strasbourg, France)
David Braun
(ICube, UMR 7357 CNRS \\ Université de Strasbourg, France)

Several tools have been developed to enhance automation of theorem proving in the 2D plane. However, in 3D, only a few approaches have been studied, and to our knowledge, nothing has been done in higher dimensions. In this paper, we present a few examples of incidence geometry theorems in dimensions 3, 4, and 5. We then prove them with the help of a combinatorial prover based on matroid theory applied to geometry.

In Predrag Janičić and Zoltán Kovács: Proceedings of the 13th International Conference on Automated Deduction in Geometry (ADG 2021), Hagenberg, Austria/virtual, September 15-17, 2021, Electronic Proceedings in Theoretical Computer Science 352, pp. 77–90.
Published: 30th December 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.352.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org