Formale Methoden zur Optimierung Nichtmonotoner Logikprogramme

Nichtmonotone logische Programme repräsentieren eine wichtige deklarative Berechnungsmethode zur Lösung komplexer Suchprobleme. Im speziellen haben logische Programme unter der Answer Set Semantik in den letzten Jahren immer mehr an Bedeutung gewonnen, was hauptsächlich auf das Vorhandensein effizienter Beweiser zurückzuführen ist. Trotz des hohen Entwicklungstandes dieser Werkzeuge besitzt die Answer Set Semantik jedoch noch einige Schwachpunkte, besonders im Hinblick auf die Vereinfachung und Optimierung von Programmen. In diesem Projekt soll auf diesen Punkt eingegangen werden, indem formale Methoden zum Vergleich und der Optimierung nichtmonotoner logischer Programme unter der Answer Set Semantik studiert werden. Im speziellen ist geplant, aufbauend auf einer systematischen Untersuchung verschiedener Begriffe der Äquivalenz, die zentral zur Behandlung von Programmoptimierung sind, einen allgemeinen Rahmen zur Spezifikation von Äquivalenzbegriffen zu bestimmen, der als theoretische Fundierung allgemeiner Optimierungsmethoden dienen soll. Dies beinhaltet im besonderen die Untersuchung formaler Eigenschaften, wie etwa semantischer und computationaler, der eingeführten Begriffe. Die entwickelten Methoden sollen dann im weiteren auf konkrete Beispielfälle angewendet werden, wobei hierfür entsprechende Prozeduren implementiert werden, die wiederum zu Prototyp-Modulen zur automatischen Programmoptimierung führen. Diese Werkzeuge können dann als Basis zur Unterstützung von Programmierern sowohl zur Fehleranalyse und Verifikation als auch zur modularen Programmierung dienen.

Nichtmonotone logische Programme repräsentieren eine wichtige deklarative Berechnungsmethode zur Lösung komplexer Suchprobleme. Im speziellen haben logische Programme unter der Answer Set Semantik in den letzten Jahren immer mehr an Bedeutung gewonnen, was hauptsächlich auf das Vorhandensein effizienter Beweiser zurückzuführen ist. Trotz des hohen Entwicklungstandes dieser Werkzeuge besitzt die Answer Set Semantik jedoch noch einige Schwachpunkte, besonders im Hinblick auf die Vereinfachung und Optimierung von Programmen. In diesem Projekt soll auf diesen Punkt eingegangen werden, indem formale Methoden zum Vergleich und der Optimierung nichtmonotoner logischer Programme unter der Answer Set Semantik studiert werden. Im speziellen ist geplant, aufbauend auf einer systematischen Untersuchung verschiedener Begriffe der Äquivalenz, die zentral zur Behandlung von Programmoptimierung sind, einen allgemeinen Rahmen zur Spezifikation von Äquivalenzbegriffen zu bestimmen, der als theoretische Fundierung allgemeiner Optimierungsmethoden dienen soll. Dies beinhaltet im besonderen die Untersuchung formaler Eigenschaften, wie etwa semantischer und computationaler, der eingeführten Begriffe. Die entwickelten Methoden sollen dann im weiteren auf konkrete Beispielfälle angewendet werden, wobei hierfür entsprechende Prozeduren implementiert werden, die wiederum zu Prototyp-Modulen zur automatischen Programmoptimierung führen. Diese Werkzeuge können dann als Basis zur Unterstützung von Programmierern sowohl zur Fehleranalyse und Verifikation als auch zur modularen Programmierung dienen.