Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Automated Reasoning in the Age of the Internet Kapitel lesen Erstes Kapitel lesen

2018 | OriginalPaper | Buchkapitel

Formalizing Some “Small” Finite Models of Projective Geometry in Coq

verfasst von : David Braun, Nicolas Magaud, Pascal Schreck

Erschienen in: Artificial Intelligence and Symbolic Computation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We study two different descriptions of incidence projective geometry: a synthetic, mathematics-oriented one and a more practical, computation-oriented one, based on the combinatorial concept of rank of a set of points. Using both axiom systems, we prove that some specific finite planes (resp. spaces) verify the axioms of projective plane (resp. space) geometry and Desargues’ property. It requires using repeated case analysis on all variables of some finite inductive data-types and leads to numerous (sub-)goals in the Coq proof assistant. We thus investigate to what extend Coq can deal with such a combinatorial explosion in the number of cases to handle. We propose some easy-to-implement but relevant proof optimizations which, combined together, lead to an efficient way to deal with such large proofs.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel A Formal Proof of the Computation of Hermite Normal Form in a General Setting
Nächstes Kapitel Into the Infinite - Theory Exploration for Coinduction
Fußnoten
1
The perspector is the point at which the three lines connecting the vertices of two perspective triangles concur.
 
2
Computer setup: Intel(R) Core(TM) i5-4460 CPU @ 3.20 GHz with 16G of memory.
 
3
An interactive representation of pg(3, 2) can be viewed on wolfram web site: http://​demonstrations.​wolfram.​com/​15PointProjectiv​eSpace/​.
 
4
Fully-specified functions can be automatically defined using the proof search capabilities of Coq.
 
Literatur
1.
Armand, M., Grégoire, G., Keller, B., Théry, L., Werner, B.: Verifying SAT and SMT in Coq for a fully automated decision procedure. In: International Workshop on Proof-Search in Axiomatic Theories and Type Theories (PSATTT 2011) (2011)
2.
Batten, L.M.: Combinatorics of Finite Geometries. Cambridge University Press, Cambridge (1997)CrossRef
3.
4.
Braun, D., Magaud, N., Schreck, P.: An equivalence proof between rank theory and incidence projective geometry. In: Automated Deduction in Geometry (ADG 2016), pp. 62–77 (2016)
5.
Buekenhout, F. (ed.): Handbook of Incidence Geometry. North Holland, Amsterdam (1995)MATH
6.
Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.6. LogiCal Project (2017)
7.
Coxeter, H.S.M.: Projective Geometry. Springer, New York (2003)MATH
8.
9.
10.
11.
12.
Magaud, N., Narboux, J., Schreck, P.: A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom.: Theor. Appl. 45(8), 406–424 (2012)MathSciNetCrossRef
13.
Mahboubi, A., Tassi, E.: Mathematical Components. Draft (2016)
14.
Michelucci, D., Schreck, P.: Incidence constraints: a combinatorial approach. Int. J. Comput. Geom. Appl. 16(5), 443–460 (2006)MathSciNetCrossRef
15.
16.
Oxley, J.G.: Matroid Theory, vol. 3. Oxford University Press, Oxford (2006)MATH
17.
18.
Tebbi, T., Gross, J.: A profiler for Ltac. In: Coq PL Workshop 2015 (2015)
Metadaten
Titel
Formalizing Some “Small” Finite Models of Projective Geometry in Coq
verfasst von
David Braun
Nicolas Magaud
Pascal Schreck
Copyright-Jahr
2018
Buch
Artificial Intelligence and Symbolic Computation

Print ISBN: 978-3-319-99956-2

Electronic ISBN: 978-3-319-99957-9

Copyright-Jahr: 2018

DOI
https://doi.org/10.1007/978-3-319-99957-9_4