Positive negative conditional equations

Thema dieser Dissertation ist das Beweisen induktiver Theoreme in Klauselform auf Basis von Spezifikationen mit konstruktorbasierten, positiv/negativ bedingten Gleichungen. Das Beweisen induktiver Theoreme ist entscheidend für die Argumentation über Computerprogramme. Angesichts der Bedeutung formaler Methoden für die Verifikation sicherheitskritischer Algorithmen ist zu erwarten, dass automatisiertes Beweisen induktiver Theoreme in naher Zukunft wirtschaftlich relevant wird. Positiv/negativ bedingte Gleichungen sind universell quantifizierte Implikationen erster Stufe, die eine einzelne Gleichung im Sukzedens und eine Konjunktion von positiven und negativen Gleichungen im Antezedens enthalten. Sie eignen sich für funktionale Spezifikationen erster Stufe und können als Programme betrachtet werden. Ein konstruktorbasierter Ansatz gibt algebraischen Spezifikationen mit diesen Gleichungen eine passende Semantik. Zudem wird eine Reduktionsrelation für positiv/negativ bedingte Regeln definiert, die die grundlegenden Ergebnisse für positiv bedingte Termersetzungssysteme beibehält. Wichtig ist, dass die Konzepte induktiver Gültigkeit gegenüber konsistenter Spezifikationserweiterung ein monotones Verhalten aufweisen. Auf dieser Grundlage wird ein Inferenzsystem zum Nachweis verschiedener induktiver Gültigkeiten von Gleichungsklauseln entwickelt. Der konstruktorbasierte Ansatz erweist sich als gut geeignet für Induktionsbeweise, auch b