Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Computergestuetzte Beweise in der Theorie verbandsgeordneter Gruppen
Date, Time and Location
Abstract
Theorembeweisern in einem mathematischen Gebiet besonders gut
geeignet. Der elementare Teil dieser Theorie laesst sich sowohl
durch eine reine Gleichungstheorie als auch durch eine Horntheorie
axiomatisieren. Die algebraischen und modelltheoretischen
Eigenschaften der verbandsgeordneten Gruppen sind gut bekannt.
Linear geordnete Gruppen bilden eine wichtige Unterklasse, die
sich nicht durch eine Horntheorie axiomatisieren laesst.
Im Vortrag werden die wichtigsten Eigenschaften verbandsgeordneter
Gruppen erlaeutert. Dabei wird besonderer Wert darauf gelegt, die
gebietsspezifischen Beweismethoden herauszuarbeiten und deren
algebraische Grundlagen darzustellen.
An Hand einer speziellen Konfiguration des Systems ILF fuer das
Gebiet der verbandsgeordneten Gruppen wird diskutiert, welchen
Beitrag automatische Theorembeweiser heute zur Entwicklung von
mathematischen Beweisen leisten koennen.
Beweise die im Computer repraesentiert werden, lassen sich auf
vielfaeltige Weise manipulieren. Insbesondere lassen sie sich
in verstaendlicher Form darstellen. Als Beispiel dafuer werden
Beweise eines Repraesentationssatzes fuer verbandsgeordnete Gruppen
vorgestellt, die von den automatischen Beweisern OTTER und DISCOUNT
gefunden wurden. Die Aufbereitung dieser Beweise macht es moeglich,
sie unter mathematischen Aspekten zu vergleichen. Auf die zur
Beweistransformation verwendeten Methoden kann eingegangen werden
soweit es der zeitliche Rahmen zulaesst.
Contact
Tags, Category, Keywords and additional notes
Tel.: (0681) 9325-227, uni-intern: 92227