Dr. H.-G. Gräbe:
Geometry Theorem Proving on the Computer
Participants:
Students of computer science and mathematics that will learn more
about applications of symbolic computations.
Credits as special course of applied or theoretical computer
science.
Overview:
In the course the audience will learn more about different
symbolic methods, that proved useful in applications to geometric
problem solving.
Structure:
- Introduction to geometric problems
- Symbolic representation of geometric constructions
- Geometry theorems of constructive type
- Geometry theorems of equational type
- Different higher algebra approaches
- Examples
Literature:
- S.-C. Chou: Mechanical geometry theorem proving. Kluwer Acad.
Publishers, Dordrecht 2002.
- S.-C. Chou u.a.: Machine Proofs in Geometry - Automated
Production of Readable Proofs for Geometry Theorems. World Scientific,
Singapore 1994 .
- D. Cox, J. Little, D. O'Shea : Ideals, varieties, and
algorithms. Springer, New York 1992.
- H.S.M. Coxeter and S.L. Greitzer : Geometry revisted. Toronto -
New York, 1967.
- W. Wu: Mechanical theorem proving in geometries. Springer, Wien
1994.
- W. Wu: Mathematics Mechanization. Reihe "Mathematics and its
Applications", Vol. 489. Kluwer Acad. Publishers, Dordrecht
2000.
Expected previous knowledge:
Good knowledge of linear algebra, basic knowledge of constructive
methods of higher algebra, in particular Gröbner bases.
Credits:
According to participation or after a test consultation.
Other :
More information (in german) about the course at
http://www.informatik.uni-leipzig.de/~graebe/vorlesungen/geometrie.html