Lösung quantifizierter Formeln aus der Regelungstechnik

Das Ziel des beantragten Projekts ist das Entwickeln von Theorien, Algorithmen und Software zum Lösen von quantifizierten Einschränkungen, die in der Regelungstechnik vorkommen. Dabei ist eine quantifizierte Einschränkung eine Formel der Prädikatenlogik erster Stufe über die reellen Zahlen. Das bedeutet, dass sie Quantoren ("für alle", "existiert"), Junktoren ("und", "oder", "nicht"), Prädikatensymbole (z.B., =, <), Funktionssymbole (z.B., +, -, *, sin), rationale Konstanten und Variablen über die reellen Zahlen enthält. In diesem Projekt fordern wir weiters, dass eine gegebene quantifizierte Einschränkung eine signifikante Anwendung in der Regelungstechnik modelliert. Das hat folgende Konsequenzen: In der Praxis sind Konstante meistens nicht exakt bekannt, also ist es wichtig, näherungsweise Eingabekonstante behandeln zu können, zum Beispiel in der Form von Gleitkommaintervallen. Weiters, sollte man näherungsweise Lösungen berechnen können, vor allem, wenn exakte Lösungen zu schwierig zu berechnen sind. Ausserdem resultieren spezielle Anwendungen in eine spezielle Struktur der auftretenden Einschränkungen. Diese Struktur kann und soll aus Effizienzgründen ausgenutzt werden.