Ein Nein kommt mit der Belegung, die die Regel bricht.

Prüft KALKÜL, ob eine Handlung die Regel R in einem Zustand S einhält, fragt es den Löser nach einer Belegung für S ∧ ¬R. Antwortet er unerfüllbar, ist die Regel bewiesen. Antwortet er erfüllbar, liefert er zugleich, was die Frage bejaht: eine Belegung, also für jede Variable einen Wert, bei dem alle Voraussetzungen gelten und die Regel nicht. Das ist das Gegenbeispiel. Es ist kein Hinweis, dass etwas schiefgehen könnte, sondern ein Zustand, in dem es schiefgeht.

Die Werte sind exakt. Über linearer Arithmetik rechnet der Löser mit rationalen Zahlen ohne Rundung, ein Wert steht als Bruch und nicht als Näherung. KALKÜL übernimmt die Belegung in dieser Form und rechnet erst für die Anzeige in Dezimalzahlen um, mit dem Hinweis, dass die Anzeige gerundet ist.

Die Belegung enthält alle Größen, die in den Voraussetzungen vorkommen, auch jene, die den Bruch nicht verursachen. Welche das sind, zeigt der Abschnitt über das kleinste Gegenbeispiel.

Ein erfüllbar vom Löser muss man nicht glauben. KALKÜL setzt die Belegung selbst in die Voraussetzungen und in die Regel ein und wertet beide in exakter Bruchrechnung aus, mit einem kleinen Programm, das mit dem Löser nichts teilt. Gelten die Voraussetzungen und bricht die Regel, ist das Gegenbeispiel bestätigt. Gilt die Regel dagegen, wird das Ergebnis des Lösers verworfen und als Fehler gemeldet. Ein Nein folgt daraus nicht.

Dieselbe Prüfung kann jede Dritte nachvollziehen. Sie braucht die Regel in der Fassung des Nachweises, den Zustand und die Belegung, keinen Löser und keinen Zugang zu KALKÜL. Das unterscheidet das Gegenbeispiel vom Beweis: Eine Belegung prüft man durch Einsetzen, für einen Beweis braucht man ein Prüfprogramm für Beweise.

Ein Löser liefert irgendeine Belegung, die genügt. Für die, die sie lesen müssen, ist das oft unbrauchbar: Es stehen viele Größen darin, von denen nur zwei den Bruch erklären. KALKÜL sucht darum die Belegung, die dem Vorschlag am nächsten liegt. Dafür dient die Optimierung, die der Löser mitbringt: Er minimiert den Abstand der Werte zum vorgeschlagenen Zustand unter der Bedingung, dass die Regel bricht.

Größen, die für den Bruch gleichgültig sind, behalten dabei ihren Wert aus dem Vorschlag. Als Unterschied bleibt, was den Bruch verursacht, und das Gegenbeispiel sagt in einer Zeile, welche Größe um wie viel zu weit geht.

Gelten mehrere Regeln, prüft KALKÜL jede einzeln und nicht nur ihre Verknüpfung. Das Ergebnis nennt alle gebrochenen Regeln mit Wortlaut, Fundstelle und Version, je mit einem eigenen Gegenbeispiel. Wer abgewiesen wird, sieht nicht nur, dass es nicht geht, sondern an welcher Vorschrift.

Rechnet KALKÜL mit Unsicherheit, ist das Gegenbeispiel kein einzelner Zustand, sondern ein Kasten aus Intervallen, in dem jeder Zustand die Regel bricht. Das ist stärker als ein Punkt, denn es zeigt, dass der Bruch nicht an einer unglücklichen Messung hängt. Die Zerlegung hält nach der Ebene an, in der sie einen solchen Kasten findet, und bestimmt näherungsweise den ersten Zeitpunkt, an dem ein möglicher Zustand die Regel bricht. So arbeitet der Demonstrator.

Bleibt ein Kasten übrig, der weder ganz erlaubt noch ganz verboten ist, ist das kein Gegenbeispiel. Das Ergebnis lautet dann unentschieden, und unentschieden heißt: keine Freigabe.

Das Gegenbeispiel ist die Eingabe der nächsten Runde. Ein Agent, der eine Handlung vorgeschlagen hat, erhält die gebrochene Regel und die Richtung des Bruchs zurück und schlägt etwas anderes vor. KALKÜL prüft den neuen Vorschlag mit denselben Regeln. Die Zahl der Runden ist begrenzt; danach geht der Fall mit allen Gegenbeispielen an eine Person.

Der Rückweg unterliegt den Rechten wie jeder andere. Enthält die Belegung Werte, die der Agent nicht lesen darf, kommen sie nicht in seinen Kontext: Er erhält die Regel und die Richtung des Bruchs, die Belegung bleibt beim Nachweis. Wo die Frage nicht Ja oder Nein lautet, sondern nach dem besten erlaubten Plan fragt, rechnet KALKÜL mit Optimierung statt mit Wiederholung.

Das Gegenbeispiel gehört zum Nachweis: Datensatz, kanonische Form, Prüfwert, Signatur, Zeitstempel. Damit ist auch das Nein prüfbar, so wie das Ja. Wer eine Handlung abgelehnt bekommt, kann die Ablehnung vor einer Stelle belegen, die KALKÜL nicht vertraut.

Eine Antwort ohne Belegung wird nie als Nein ausgegeben. Läuft der Löser in die Zeitgrenze oder bleibt eine Zerlegung offen, lautet das Ergebnis unentschieden. Das ist ein eigener Zustand mit eigener Folge: keine Freigabe, aber auch kein Vorwurf an die Handlung. Wer Nein sagt, muss es zeigen können.