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...
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