Auf den ersten Blick scheint es nicht besonders schwierig zu sein, in einer
Sprache der Prädikatenlogik Situationen und Aktionen zu formalisieren und
mittels der Inferenzregeln Pläne auszurechnen. Betrachten wir dazu den
Gentzen-Kalkül 
, wie er zB. in [Gal86] oder in [Bib92] beschrieben ist. Die Ausgangssituation, zB. die Tatsache,
daß Eisen vorhanden ist, läßt sich darin als
formalisieren, wobei das nullstellige Prädikatszeichen Fe für das Vorhandensein von Eisen steht. Die Aktionen füge_Schwefel_hinzu und erhitze_Eisen_und_Schwefel können durch die folgenden beiden Sequenzen angegeben werden.
Diese Formalisierung sieht zwar sehr natürlich aus, jedoch kann, wie in Abbildung 4.17 gezeigt ist, die Sequenz
unter Verwendung der Eigenaxiome (4.9) und (4.10) abgeleitet
werden. In Worten besagt dies, wenn Schwefel zu Eisen hinzugefügt und
anschließend das Gemisch erhitzt wird, dann entsteht zwar Schwefeleisen,
aber Eisen und Schwefel bleiben erhalten! Das widerspricht allen Erkenntnissen
der Chemie. Die Ursache für diesen Effekt liegt in den beiden Anwendungen
der
Abschwächungsregel
in der in Abbildung 4.17 gezeigten Ableitung, die dort mit
gekennzeichnet sind. Wenn wir jedes Vorkommen eines
Prädikatszeichens in einer Sequenz als Ressource betrachten, dann bedeutet
die Anwendung der Abschwächung ja gerade, daß wir neue Ressourcen quasi
aus dem Nichts erzeugen. Umgekehrt bewirkt die in vorhandene
Kürzungsregel,
daß Ressourcen verschwinden. Wir werden im Abschnitt 4.7.5 über
Lineare Logik noch einmal auf
die Bedeutung der Abschwächung und der Kürzung zurückkommen. Jedoch sei
schon an dieser Stelle darauf hingewiesen, daß ohne Verwendung der
Abschwächung und der Kürzung eine Ableitung von (4.11) in nicht möglich ist.
Abbildung 4.17: Ein Beweis für 
im Gentzen-Kalkül mit den
Eigenaxiomen (4.9) and (4.10). 
,
und 
bezeichnen die Abschwächung links, die
Konjunktion rechts und den Schnitt (siehe zB. [Gal86] oder
[Bib92]).
Christoph Quix, Thomas List, René Soiron
