Kurzfassung

Symbolelimination im Allgemeinen und Quantorenelimination
insbesondere sind heutzutage in verschiedenen Bereichen
wichtig: In der Verifikation wird Symbolelimination
z.B. in CEGAR Verfahren (Counterexample-Guided Abstraction
Refinement) oder in der automatischen Generierung von
Invarianten benutzt. In der Verifikation von Parametrischen Systemen
ist es oft wichtig, Constraints auf Parameter zu generieren, die
die Sicherheit solcher Systeme gewährleisten.
In Datenbanken wird Symbolelimination...Symbolelimination im Allgemeinen und Quantorenelimination
insbesondere sind heutzutage in verschiedenen Bereichen
wichtig: In der Verifikation wird Symbolelimination
z.B. in CEGAR Verfahren (Counterexample-Guided Abstraction
Refinement) oder in der automatischen Generierung von
Invarianten benutzt. In der Verifikation von Parametrischen Systemen
ist es oft wichtig, Constraints auf Parameter zu generieren, die
die Sicherheit solcher Systeme gewährleisten.
In Datenbanken wird Symbolelimination benutzt um das ``Vergessen''
zu modellieren. In der Mathematik werde solche Verfahren
insbesondere für das automatische Beweisen von
Theoremen in der analytischen Geometrie benutzt.

Das Ziel dieses Projektes ist es, Methoden zur Symboleliminitation und
Quantorenelimination in verschiedenen Theorien zu untersuchen.
Letztendlich möchten wir Methoden für die Symbolelimination in
komplexen Theorien entwickeln, welche die
modulare Struktur der Theorien ausnutzen und es erlauben, spezialisierte
Methoden für Symbolelimination und/oder
Quantorenelimination für einzelne Theorien modular zu
benutzen, und Anwendungen solcher Methoden in der
Verifikation, in der Analyse von Datenbanken und in der
Geometrie zu analysieren.» weiterlesen» einklappen