New for: D1, D2, D3, D4, D5
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.