Effiziente Erkennung ähnlicher Sequenten

Event-B ist eine Notation zur formalen Modellierung computerbasierter Systeme. Zur systematischen Analyse der Modelle dienen Beweisobligationen: Sequenten, die aus Elementen des Modells kombiniert werden. (Ein Sequent ist eine Formel der Form H |- C, wobei H eine Liste von Hypothesen ist und C das Beweisziel.) Jeder dieser Sequenten kann durch eine kleine Menge bestimmender Elemente identifiziert werden.

Beispiel: Ein Modell besteht aus eine Liste von Invarianten I_1, I_2, ..., I_n und einer Liste von Ereignissen der Form (G_k --> x := A_k) für 1 <= k <= m. Dann ist zu beweisen, daß sämtliche Ereignisse alle Invarianten erhalten. Das entspricht den Sequenten:

I_1, I_2, ..., I_n, G_k |- I_j[x := A_k] für 1 <= j <= n, 1 <= k <= m.

Die bestimmenden Elemente dieses Sequenten sind G_k, I_j, x, A_k.

Nun kommt es häufig vor, daß ein Modell editiert werden muß; ein fehlschlagender Beweis oder ein Tippfehler können zum Beispiel Ursachen sein. Ein wichtiges Problem in der praktischen Anwendung von Event-B ist das schnelle auffinden alter Beweisobligationen nachdem eine Änderung an einem Modell vorgenommen wurde. Die notwendige Suche muß natürlich solchen Änderungen Rechnung tragen und sollte robust genug sein eine alte Beweisobligation wiederzufinden. Der praktische Wert in einem Softwarewerkzeug für Event-B liegt im Wiederfinden bereits durchgeführter Beweise und im Finden von Beweisen ähnlicher Beweisobligationen, die bereits geführt wurden. Dadurch kann der Benutzer des Werkzeugs den Aufwand sparen Beweise mehrmals zu führen.

Mögliche Techniken zur Suche:

(1) Abgestufte Äquivalenz: Gewichtete Suche in Teilbäumen, z.B.:

y = x * 2 ~v~ y = (5 + z) * 2
y = x * 2 ~w~ y = (x * 2) + 1

v und w sind dabei numerische Werte, die die Ähnlichkeit der Formeln ausdrücken.

(2) Umbenennung von Bezeichnern:

y = k + 1 ~u~ w = m + 1

(3) Para-Modulation:

y = (a + b) + c ~r~ y = a + (b + c)

(4) Normalisierung:

k + 1 = y ~s~ y = k + 1
k < y ~q~ y >= k + 1

Möglicherweise bieten sich während der Arbeit weitere Techniken an oder es stellt sich heraus, das einige nicht den gewünschten Effekt haben.

Die Effizienz der implementierten Suche anhand vorher festgelegter Testfälle evaluiert werden. Die Implementierung sollte in einer deklarativen Programmiersprache wie Prolog oder Haskell erfolgen.