A decision procedure for geometry in Coq
In: TPHOLS 2004 : theorem proving in higher order logics (Park City UT, 14-17 September 2004)Lecture notes in computer science :225-240
Konferenz
- print, 18 ref
Zugriff:
We present in this paper the development of a decision procedure for affine plane geometry in the Coq proof assistant. Among the existing decision methods, we have chosen to implement one based on the area method developed by Chou, Gao and Zhang, which provides short and readable proofs for geometry theorems. The idea of the method is to express the goal to be proved using three geometric quantities and eliminate points in the reverse order of their construction thanks to some elimination lemmas.
Titel: |
A decision procedure for geometry in Coq
|
---|---|
Autor/in / Beteiligte Person: | NARBOUX, Julien |
Link: | |
Quelle: | TPHOLS 2004 : theorem proving in higher order logics (Park City UT, 14-17 September 2004)Lecture notes in computer science :225-240 |
Veröffentlichung: | Berlin: Springer, 2004 |
Medientyp: | Konferenz |
Umfang: | print, 18 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|