Das Thema meiner Studienarbeit lautet „Ein Entscheidungsverfahren für die Presburger Arithmetik”. Es handelt sich um eine Arbeit in der Disziplin der theoretischen Informatik.
Der Kern meiner Studienarbeit ist das Eliminieren von (Existenz−) Quantoren. Sobald eine Formel der Presburger Arithmetik quantorenfrei ist, ist der Rest des Beweises nur noch trivial.
Der praktische Teil meiner Studienarbeit ist die Entwicklung eines Programms, das einen automatischen Beweis führt (siehe Applet).

Diese Frage höre ich oft, wenn ich von meiner Studienarbeit erzähle. Doch im Prinzip wendet absolut jeder diese Arithmetik tagtäglich an. Es bezeichnet das Plus- und Minusrechnen mit ganzen Zahlen (ohne Multiplikation, ohne Division), also praktisch Kinderkram. :−)

Hier können Sie eine automatisiert getestete Version meines Beweisers nutzen. Über Rechtsklick ist es möglich, eine Reihe von Aktionen auf den Syntaxbaum anzuwenden. Mittels „Drag−And−Drop” können Formeln des Syntaxbaumes auch in den Eingabebereich geschoben werden.

Im Folgenden sehen Sie die kontextfreie Grammatik, die die Sprache zum Applet beschreibt. Diese Sprache habe ich im Zuge der Realisierung des Entscheidungsverfahrens konstruiert. Ich gab ihr den Namen

1. PAQL (Presburger Arithmetik Query Language). {Damit keine Verwechslungen mit der Peano-Arithmetik entstehen, darf anstelle von PAQL auch PrAQL notiert werden. Nebenbei bemerkt, PAQL deckt syntaktisch jedoch auch den Sprachumfang der unentscheidbaren Peano-Arithmetik ab.}

//Produktionen equivalences ::= implications { "<->" implications } . implications ::= disjunctions { "->" disjunctions } . disjunctions ::= conjunctions { ("or"|";") conjunctions } . conjunctions ::= formula { ("and"|",") formula } . formula      ::= "not" formula                | "forall" VAR { "," VAR } [":"|"."] formula                | "exists" VAR { "," VAR } [":"|"."] formula                | "true"                | "false"                | sum { ("="               // gleich                        |"!="|"<>"         // ungleich                        |"<"|">"|"<="|">=" // klar!                        |"#" NAT           // kongruent                        |"!#" NAT          // nicht kongruent                        |"|"               // teilt                        |"!|"              // teilt nicht                        ) sum }+                | "(" equivalences ")" . sum          ::= ["+"|"-"] product { ("+"|"-") product } . product      ::= successor { ["*"] successor } . successor    ::= term { "'" } . term         ::= NAT | VAR | "(" sum ")" . // Startsymbol einer Formel equivalences. // Startsymbol eines Terms sum. // Besondere Terminale VAR steht für einen typischen Variablenbezeichner. NAT steht für eine natürliche Zahl.

Folgende Beispiele können Sie gerne mit dem Applet austesten.

• forall x exists y (x=2*y or x=(2*y)')
  Jede Zahl x ist gerade oder ungerade.
• forall x ((2|x and 3|x) -> 6|x)
  Ist eine Zahl x durch 2 und 3 teilbar, so ist x auch durch 6 teilbar.
• forall x (3|x -> 6|x+x)
  Ist eine Zahl x durch 3 teilbar, dann ist x + x durch 6 teilbar.
• forall x exists y x<y<x''
  Für jede Zahl x gibt es eine Zahl y, die größer als x und zugleich kleiner als x + 2 ist.
• exists A,B (A=9 and B=11 -> exists x A<x<B and not exists y,z A<y<z<B)
  Zwischen den Grenzwerten 9 und 11 existiert genau eine Zahl.
• exists n forall x (0<n<x -> exists a,b x=6*a+7*b)
  Ab einer bestimmten positiven Zahl n lässt sich jede Zahl x als Linearkombination mit zwei gegebenen, teilerfremden Zahlen 6 und 7 darstellen.

Besonders interessant ist es, wenn Sie den Entscheider auf Formeln mit freien Variablen anwenden. Ähnlich wie bei Prolog ist eine Aussage mit freien Variablen als Query zu verstehen. Das Ergebnis kann folgende Formen annehmen:

1. true
   Jede Belegung (aller freien Variablen) macht aus der gegebenen Formel einen wahren Satz.
2. false
   Es gibt keine Belegung (aller freien Variablen), die aus gegebener Formel einen wahren Satz macht.
3. Wiederum eine offene Formel
   Für eine beliebige Belegung (aller freien Variablen) werden die Ausgangsformel und die Ergebnisformel zu äquivalenten Sätzen.

Im Folgenden erfahren Sie ein paar interessante Beispielformeln:

• e+e=e
  Wie lautet das neutrale Element e bezüglich der Addition?
• exists a,b (0<a, 0<b, x=5*a+7*b)
  Welche Zahl kann man für die Variable x einsetzen, damit die gegebene Linearkombination zu einem wahren Satz wird?
• exists a (0<a<b, x=a+2*b)
  Welche Zahlen kann man für die Variablen x und b einsetzen, damit die gegebene Formel zu einem wahren Satz wird?
• exists x x+x+y=z
  Wie müssen die Variablen y und z belegt werden, dass die gegebene Formel zu einem wahren Satz wird?
• exists x (x<z, x<y<z)
  Kommt nun y < z als Ergebnisformel heraus, wissen wir, dass in dieser Arithmetik die Transitivität gilt.

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:

1. Bernd, Peter und Susi machen einen Gewichtsvergleich.
   1. Bernd ist doppelt so schwer wie Peter.
   2. Bernd wiegt 10 kg weniger als Susi.
   3. 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.

1. Die Kurzfassung zu den drei Existenzquantoren hat folgende Form: 'exists Bernd, Peter, Susi'.
2. 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.
3. 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.

1. Sie fügen ein weiteres Konjunktionsglied ein, wie etwa 'X = Bernd', dann steht X für das Gewicht von Bernd.
2. 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.

Folgende lustige Aufgabe wurde von einem Mathematikprofessor an der Universität von Barcelona gestellt:

• Eine Mutter ist 21 Jahre älter als ihr Kind und
• in sechs Jahren wird das Kind fünfmal jünger sein, als die Mutter.
• Wo ist der Vater?

Diese Aufgabe scheint ein Scherz zu sein, doch sie ist tatsächlich lösbar und gar nicht so schwer.
Achtung: Bitte nicht weiterlesen, wenn Sie diese Aufgabe ohne fremde Hilfe lösen möchten!


Es gibt viele Herangehensweisen, um auf die richtige Lösung zu kommen: Man nimmt die Jogahaltung ein, stellt sich auf den Kopf oder schiebt sich eine Karotte in den Po, oder man macht all jenes gleichzeitig, um ganz entspannt auf die richtige Lösung zu kommen. Diese Anmerkung kann ich mir an dieser Stelle einfach nicht verkneifen, ich hoffe, Sie verstehen das! :−)
Gehen Sie doch einfach ganz formal an die Sache heran, schlagen Sie doch den bequemeren Weg des automatischen Beweisens ein! Diese Denksportaufgabe kann nämlich auch wissenschaftlich — wer hätte das gedacht — mit dem vorliegenden Presburger Entscheider gelöst werden, indem man wie folgt erst einmal das Alter des Kindes bestimmt.

exists Mutter (   Mutter = Kind + 21,   Mutter + 6 = 5 * (Kind + 6) )

Wenn Sie diese Formel dem Beweiser übergeben, können Sie das Ergebnis fast ablesen: Das Kind ist −3/4 Jahre alt. Wenn Sie das Ergebnis in Monate umrechnen, können Sie rasch folgern, auf wem … äh, wo sich der Vater befindet. :−)

Wenn Sie sich nun für meine Studienarbeit interessieren sollten, können Sie Näheres in den folgenden herunterladbaren PDF−Dateien erfahren.

Download: Eine Möglichkeit an die hier vorgestellte Studienarbeit heranzukommen.

1. Studienarbeit.pdf (271.018 Bytes)
2. Studienarbeit.pdf mit Javacodes (2.945.036 Bytes)

Auch wenn meine Ausarbeitung stellenweise den Eindruck von Halbherzigkeit vermitteln sollte, so kann ich Ihnen versichern, dass ich bei der Entwicklung des obigen Java−Applets keine Mühen gescheut und alle Register meines bisherigen Studiums gezogen habe, um ein überwältigendes Werk zu schaffen. In diesem zugegebenermaßen unscheinbar wirkenden Applet verbirgt sich enorm viel KnowHow, was die Software−Technik anbelangt.

• Adäquate Realisierung der zugrundeliegenden Theorie,
• erfinderische Konstruktion einer intuitiven Abfragesprache (PAQL),
• gezielter Einsatz von geeigneten Entwurfsmustern (z. B.: Composite und Visitor),
• gewissenhafte Qualitätssicherung durch automatisiertes Testen (Löwenanteil),
• visuelle Kontrolle durch Einsatz von „Graphviz” (DotCode),
• konsequente Einhaltung der Java−Programmierrichtlinien und nichtsdestoweniger
• bewusste Trennung von Benutzerschnittstelle und Funkionalität (Swing)

machten das Applet zu dem, was es heute ist. Es wäre also schade, wenn Sie die vorliegende Arbeit nicht ein wenig unter die Lupe nehmen würden. Mein Betreuer meinte, ich könne wahrhaft stolz auf meine Arbeit sein: „Sie haben ein vollständiges Entscheidungsverfahren für die Presburger Arithmetik realisiert. Was haben Sie nur gemacht, dass es nun endlich funktioniert?” :−)

Für weitere Detailfragen sollten Sie sich direkt an den Lehrstuhl für Systemsimulation der Friedrich−Alexander−Universität wenden. Dort habe ich nämlich meine Studienarbeit geschrieben.
Selbstverständlich stehe auch ich persönlich für dringende Fragen zur Verfügung. Ich bin immer wieder glücklich, wenn ich jemanden helfen kann. Umgekehrt wäre es aber auch schön, wenn Sie PAQL zu einem Wikipedia−Eintrag verhelfen könnten.
Herzlichst, Stefan Karl Baur

Bei dieser Studienarbeit gab es viele Hürden zu überwinden, die ich vielleicht ohne Unterstützung gar nicht gemeistert hätte.

An dieser Stelle bedanke ich mich bei jenen, die mir besonders gut zum Ziel verholfen haben.

• Arne Becker, der mich immer wieder zum Weitermachen motiviert hat. Danke Arne!
• Thomas Bertz, der mir immer wieder gute Tipps zum Beweiser gegeben und eine meiner vorläufigen Arbeiten Korrektur gelesen hat. Danke Thomas!
• Dr. Degen, meinem Betreuer, der mich immer wieder auf das Wesentliche zurückgeführt hat. Danke Dr. Degen!
• Hellmuth Klohs, der mich zum obigen Tutorium „Textaufgaben für Schüler” inspirierte. Durch ihn habe ich eine völlig neue Sicht auf das Ganze bekommen. Danke Hellmuth!