Projekt: Algebra

Thema: Automatisches Beweisen in der Geometrie

Erhard Aichinger, Zoltan Kovacs


Satz von Desargues

Viele Sätze der ebenen Geometrie (Thales, Desargues, Pappus, Ceva) lassen sich, mit Computerhilfe, "automatisch" beweisen, etwa, indem man die Voraussetzungen und Behauptungen in ein Gleichungssystem übersetzt und die Lösbarkeit dieses Systems überprüft.

Im vorliegenden Projekt werden einige geometrische Sätze vorgestellt und verschiedene Beweismethoden untersucht.

Eine solche Methode, die auf Sätzen von David Hilbert und Bruno Buchberger aufbaut, wird im Detail vorgestellt, und von den Teilnehmern verwendet, um eigenständig Computerbeweise einiger Sätze der Geometrie zu entwickeln. Dazu werden Gröbnerbasen verwendet; Gröbnerbasen bieten eine Möglichkeit, auch nichtlineare Gleichungssysteme algorithmisch zu lösen.

 


Abschlusspräsentation der Gruppe Algebra/ Automatisches Beweisen in der Geometrie,
siehe auch prezi.com

Aufnahme der Teilnehmer