Oft werde ich gefragt, wozu man denn die Presburger Arithmetik brauche.
Ich muss mir selbst eingestehen, dass ich bei dieser Frage anfangs immer ins Schleudern geriet.
Doch je länger ich mich mit diesem Thema befasste, desto mehr Anwendungsfälle fand ich.
Ließe sich zum Beispiel ein Computerprogramm in eine Formel der Presburger Arithmetik übersetzen,
so hätte man mit dem vorliegenden Beweiser eine Möglichkeit, das Programm zu beweisen.
Wenn ein netter Mathematiklehrer für seine Schüler eine Textaufgabe erstellt,
möchte er bestimmt auch,
dass seine Schüler auf ganzzahlige Ergebnisse kommen.
Und da die Presburger Arithmetik nur ganze Zahlen kennt,
kann er zur Formulierung einer Textaufgabe vorliegenden Beweiser verwenden.
Dies will ich anhand eines Beispiels tutoriumartig demonstrieren.
Als Beispiel soll nun folgende Textaufgabe dienen:
- Bernd, Peter und Susi machen einen Gewichtsvergleich.
- Bernd ist doppelt so schwer wie Peter.
- Bernd wiegt 10 kg weniger als Susi.
- Zusammen wiegen sie 210 kg.
Wie viel wiegt jeder Einzelne?
Es handelt sich um den Aufgabentyp
„3 Gleichungen mit 3 Unbekannten”.
exists Bernd exists Peter exists Susi
(
Bernd = Peter + Peter // Bernd ist doppelt so schwer wie Peter.
and
Bernd = Susi - 10 // Bernd wiegt 10 kg weniger als Susi.
and
Bernd + Peter + Susi = 210 // Zusammen wiegen sie 210 kg.
)
Wenn diese Formel für Sie etwas länglich erscheinen sollte,
so können Sie hier auch eine etwas prägnantere und zugleich intuitivere Schreibweise
(Syntactic Sugar)
anwenden.
- Die Kurzfassung zu den drei Existenzquantoren hat folgende Form:
'exists Bernd, Peter, Susi'.
- Die Presburger Arithmetik kennt zwar keine allgemeine Multiplikation,
jedoch lässt sich eine Multiplikation mit einer Konstante bekanntlich in eine Summe umformulieren.
Deshalb ist es auch legitim, statt
'Peter + Peter'
auch
'2 * Peter'
oder auch
'Peter * 2'
zu schreiben.
- Das Schlüsselwort der Konjunktion
'and'
kann durch ein einfaches Komma ersetzt werden.
Nebenbei bemerkt kann das Oder
'or'
mit einem Semikolon notiert werden.
Die verkürzte Fassung sieht wie folgt aus.
exists Bernd, Peter, Susi
(
Bernd = 2 * Peter, // Bernd ist doppelt so schwer wie Peter.
Bernd = Susi - 10, // Bernd wiegt 10 kg weniger als Susi.
Bernd + Peter + Susi = 210 // Zusammen wiegen sie 210 kg.
)
Diese Formel ist entweder wahr
(true)
oder falsch
(false).
Wenn die Formel wahr ist,
so existiert für jede Variable
(Bernd, Peter und Susi)
eine ganzzahlige Lösung,
andernfalls liegt für mindestens eine Variable keine ganzzahlige Lösung vor.
Rein theoretisch könnten die Ergebnisse unrealistisch sein.
Um zu verhindern, dass beispielsweise eine Person nur 2 kg wiegt oder eine andere 500 kg schwer ist,
sollten Sie zusätzlich Nebenbedingungen
(Constraints)
in die Formel zur Textaufgabe integrieren.
Diese Nebenbedingungen geben dem Schüler eine weitere Unterstützung zur Plausibilitätsprüfung seiner Ergebnisse.
exists Bernd, Peter, Susi
(
Bernd = 2 * Peter, // Bernd ist doppelt so schwer wie Peter.
Bernd = Susi - 10, // Bernd wiegt 10 kg weniger als Susi.
Bernd + Peter + Susi = 210, // Zusammen wiegen sie 210 kg.
/* Jeder Einzelne wiegt mindestens 30 kg und weniger als 100 Kg. */
30 <= Bernd < 100,
30 <= Peter < 100,
30 <= Susi < 100
)
Wenn Sie nun wissen wollen, ob Ihre Lösung korrekt ist,
dann sollten Sie die Konjunktion um Ihre Lösung erweitern.
Im Anschluss sollten Sie erneut beweisen
(true, Lösung korrekt).
exists Bernd, Peter, Susi
(
Bernd = 2 * Peter, // Bernd ist doppelt so schwer wie Peter.
Bernd = Susi - 10, // Bernd wiegt 10 kg weniger als Susi.
Bernd + Peter + Susi = 210, // Zusammen wiegen sie 210 kg.
/* Jeder Einzelne wiegt mindestens 30 kg und weniger als 100 Kg. */
30 <= Bernd < 100,
30 <= Peter < 100,
30 <= Susi < 100,
/* Ihre Probe. */
Bernd = 80,
Peter = 40,
Susi = 90
)
Bisher waren die Formeln geschlossen,
d. h. sie enthielten keine freien Variablen,
d. h. jede Variable war an einen
(Existenz-)
Quantor gebunden.
Enthält aber die Formel freie Variablen, also ungebundene Variablen,
dann erhalten Sie nach dem automatischen Beweis entweder
'true'
(für die freien Variablen kann jede beliebige Ganzzahl eingesetzt werden)
- oder
'false'
(es gibt keine ganzzahlige Belegung für die freien Variablen)
- oder
eine neue Formel mit mindestens einer freien Variable.
Doch Vorsicht: Die neue Formel kann auch kompliziert und lang sein.
Im seltensten Fall kann die Lösung direkt abgelesen werden.
Doch eine kompliziertere Lösung kann einen netten Mathematiklehrer zu weiteren Teilaufgaben
und einen ganz besonders netten zu Kontrollhilfen inspirieren, wie beispielsweise:
Das Gewicht von Susi ist durch 6 teilbar.
Um sich nun die Lösung für Bernd ausgeben zu lassen, gibt es zwei Möglichkeiten.
- Sie fügen ein weiteres Konjunktionsglied ein, wie etwa
'X = Bernd',
dann steht X für das Gewicht von Bernd.
- Oder Sie heben die Bindung von Bernd auf.
Im Folgenden sind die beiden Möglichkeiten als Formeln realisiert.
/* Offene Formel mit X als freie Variable. */
exists Bernd, Peter, Susi
(
Bernd = 2 * Peter, // Bernd ist doppelt so schwer wie Peter.
Bernd = Susi - 10, // Bernd wiegt 10 kg weniger als Susi.
Bernd + Peter + Susi = 210, // Zusammen wiegen sie 210 kg.
/* Ein freies X für das Gewicht von Bernd. */
X = Bernd
)
/* Offene Formel mit Bernd als freie Variable. */
exists Peter, Susi
(
Bernd = 2 * Peter, // Bernd ist doppelt so schwer wie Peter.
Bernd = Susi - 10, // Bernd wiegt 10 kg weniger als Susi.
Bernd + Peter + Susi = 210 // Zusammen wiegen sie 210 kg.
)
Sie sollten andere oder auch weitere Bindungen aufheben, um zu sehen, was weiter geschieht.