Regeln als Formeln.

Eine Regel wird aus ihrem Wortlaut in eine formale Bedingung übersetzt: Variablen für die Größen von Zustand und Handlung, ihre Wertebereiche, Boolesche Verknüpfungen (und, oder, nicht, wenn dann) und lineare Ungleichungen über Zahlen. Aus dem Satz, eine Größe bleibe über ihrer Mindestgrenze, solange keine Freigabe vorliegt, wird etwa ¬f → x ≥ x_min.

Jede Regel trägt ihren Wortlaut, ihre Fundstelle in der Vorschrift und eine Version. Die Übersetzung prüfen Fachleute an Beispielen: Für eine Reihe von Zuständen, deren richtige Antwort feststeht, muss die Formel dasselbe sagen wie der Wortlaut. Erst dann geht die Version in Betrieb.

KALKÜL übergibt Zustand, Handlung und Regeln an einen SMT-Löser (Satisfiability Modulo Theories), etwa Z3. Ein SMT-Löser entscheidet, ob eine Formel über Theorien wie lineare Arithmetik, Bitvektoren oder Arrays eine erfüllende Belegung hat. Für lineare Arithmetik über ganzen und über rationalen Zahlen ist diese Frage entscheidbar; der Löser antwortet erfüllbar (sat) oder unerfüllbar (unsat), sofern er im Rechenbudget fertig wird.

Eingabe ist SMT-LIB, das gemeinsame Format der Löser. Dieselbe Prüfung lässt sich darum mit einem zweiten, unabhängig entwickelten Löser wie cvc5 gegenrechnen. Stimmen beide überein, hängt das Ergebnis nicht an einem einzelnen Programm.

Um zu zeigen, dass eine Regel R für alle erlaubten Zustände gilt, fragt KALKÜL den Löser nach dem Gegenteil: Gibt es einen Zustand, der die Voraussetzungen S erfüllt und R verletzt, also eine Belegung für S ∧ ¬R? Antwortet der Löser unerfüllbar, gibt es keinen solchen Zustand. R gilt dann für jeden Zustand, den S zulässt, nicht nur für die ausprobierten.

Löser wie cvc5 können zum Ergebnis unsat einen Beweis ausgeben, etwa im Format Alethe, den ein kleines, eigenständiges Prüfprogramm nachrechnet. Vorgesehen ist, diesen Beweis dem Nachweis beizulegen. Für den Schritt von der Formel zum Ergebnis muss man dann weder KALKÜL noch dem Löser glauben, sondern nur dem Prüfprogramm; dass die Formel die Vorschrift richtig wiedergibt, bleibt Sache der fachlichen Prüfung.

Antwortet der Löser erfüllbar, liefert er eine erfüllende Belegung aller Variablen, die S erfüllt und R bricht. Das ist ein Zustand, den die Voraussetzungen zulassen; für ein Nein reicht das. KALKÜL übersetzt ihn zurück in die Begriffe der Ontologie: welche Regel, welche Größen mit welchen Werten, zu welchem Zeitpunkt.

Ein Gegenbeispiel lässt sich ohne Löser nachprüfen: Man setzt die Werte in Voraussetzungen und Regel ein und rechnet. Das macht es zum stärksten Grund für ein Nein, und zum genauesten Hinweis, was an der Handlung zu ändern wäre.

Regeln über Abläufe, die für jeden Zeitpunkt gelten sollen, übersetzt KALKÜL in eine Folge von Zuständen über einem Zeitraster mit fester Schrittweite. Die Variablen gibt es je Schritt, und die Dynamik verknüpft Schritt mit Schritt. Für einen begrenzten Horizont ist das wieder eine gewöhnliche SMT-Formel; das Verfahren heißt beschränkte Modellprüfung. Ein Nachweis gilt dann für die Rasterpunkte bis zum Horizont. Für die Zeit dazwischen braucht es eine Schranke der Änderung je Schritt, die in die Grenze eingerechnet wird, für unbegrenzte Zeit eine Invariante, gezeigt per Induktion (k-Induktion).

Nicht jede Regel ist linear. Produkte von Variablen, Exponentialfunktionen oder Wurzeln führen in nichtlineare Arithmetik, in der Löser langsam werden oder keine Antwort finden. Solche Bedingungen rechnet KALKÜL mit Intervallen.

Jede Prüfung hat ein Rechenbudget. Wird es überschritten, lautet das Ergebnis unentschieden, und unentschieden ist kein Ja: Die Handlung wird nicht freigegeben, solange die Rechnung kein Ergebnis hat. Der Demonstrator auf der Seite von KALKÜL rechnet nach dem Muster der Intervalle, nicht mit einem SMT-Löser.