Teil IV: Algorithmische Logik

In diesem letzten Beitrag zur Geschichte der Logik wollen wir auf eine moderne Entwicklung der mathematischen Logik etwas genauer eingehen.

Es ist eine bekannte Tatsache, daß sich bei der gegenwärtigen hochentwickelten Rechentechnik die Tendenz zeigt, daß im Rahmen der Kosten einer rechentechnischen Anlage der Anteil der Kosten für die Software (Systemunterlagen) gegenüber den Kosten für die Hardware (Gerätetechnik) zunehmend größer wird und heute meist schon weit mehr als 50 Prozent der Gesamtkosten ausmacht. Dies ist eine der Ursachen für die gegenwärtigen äußerst vielfältigen theoretischen Untersuchungen auf dem Software-Sektor, die weltweit durchgeführt werden. Ihre Resultate und Bemühungen kann man der sogen. Programmierungstheorie zuordnen. Wie bei jeder speziellen mathematischen Theorie war man auch hier bestrebt, eine logische Grundlage für diese Theorie zu schaffen, die Programmierungstheorie als ein formalisiertes System darzustellen. So entwickelte sich die algorithmische Logik. Ihr Anliegen ist das Auffinden und Formulieren der wichtigsten Gesetzmäßigkeiten, die Berechnungsprozesse betreffen, unabhängig von konkreten Maschinen oder Algorithmen, Programmiersprachen und Berechnungsobjekten. Sie beschäftigt sich mit Berechnungen, Datenstrukturen usw. Ihre Resultate können angewandt werden bei der Analyse von Programmen, speziell bei der Verifikation von Eigenschaften von Programmen, in der Theorie der Datenstrukturen, der Algorithmentheorie, der Kompliziertheitstheorie, beim Algorithmenentwurf, dem Aufbau von Programmiersprachen u.a. Die zu untersuchenden Gesetzmäßigkeiten ähneln dabei den Gesetzen der Aussagenlogik und Prädikatenlogik, und der Aufbau des Systems der algorithmischen Logik ist analog dem Aufbau einer jeden formalisierten prädikatenlogischen Sprache.

Erste Untersuchungen von Programm-Eigenschaften mit Mitteln der Logik finden wir in den Jahren 1959 bzw. 1962 bei dem sowjetischen Mathematiker J. I. Janow und dem Amerikaner J. McCarthy. Janow entwickelte ein System für das Beweisen der Äquivalenz von Programmen und McCarthy für die Korrektheit von Programmmen. Zwei Programme heißen äquivalent, wenn sie die gleichen Ergebnissse liefern. Ein Programm heißt korrekt bezüglich zweier Eigenschaften A und B, wenn die Gültigkeit von A für die Eingangsdaten des Programms die Gültigkeit von B für die Ausgangsdaten zur Folge hat.

Ein erstes logisches System, das geeignet ist, allgemeine Programmeigenschaften zu untersuchen bzw. zu beschreiben, enthält eine 1966 erschienene Monographie von Helmut Thiele, einem Schüler von Karl Schröter. Dieses Buch mit dem Titel „Wissenschaftstheoretische Untersuchungen in algorithmischen Sprachen” wird gelegentlich als Ursprung der algorithmischen Logik bezeichnet. Ausgangspunkt für Thiele war eine graphentheoretische Beschreibung algorithmischer Prozesse durch Lev A. Kaloujnine (Kiew). Die Formalisierung erfolgte durch eine Erweiterung des üblichen Prädikatenkalküls der ersten Stufe. Nebenbei bemerkt, sind der Name Helmut Thieles (geb. 1926) und die Jahreszahl 1966 aus anderem Grunde auch für die Universität Jena bedeutungsvoll. Nachdem 1966 die Sektion Mathematik der Friedrich-Schiller-Universität Jena als erste Mathematik-Sektion im Hochschulwesen der DDR gegründet wurde, war Professor Thiele ihr erster Sektionsdirektor.

1967 zeigte der Schweizer Erwin Engeler, daß gewisse Terminations-Eigenschaften von Programmen (das sind Eigenschaften, nach denen ein Programm überhaupt zu einem Ergebnis gelangt) in gewissen logischen Systemen ausgedrückt werden können. Die Arbeiten von Engeler waren 1968 der Ausgangspunkt für eine Gruppe von Wissenschaftlern der Universität Warschau, sich mit der algorithmischen Logik zu beschäftigen. Diese Warschauer Schule unter Leitung von Andrzej Salwicki gilt inzwischen im Weltmaßstab als eine der führenden Gruppen auf diesem Gebiet. Ihr gehören ferner an L. Banachowski, A. Kreczmar, G. Mirkowska, H. Rasiowa und viele andere. Gegenwärtig finden wir Forschungen zur algorithmischen Logik überall, wo theoretische Computerwissenschaft betrieben wird. Besonders starke Zentren gibt es neben Polen noch in den USA und in der Sowjetunion. Das Gebiet der algorithmischen Logik hat sich dabei selbst zu einer vielfältigen Wissenschaft entwickelt, in der unterschiedlichste Logiksysteme untersucht werden, die schon heute kaum noch von einzelnen Wissenschaftlern überblickt werden können. Von McCarthy stammt der zukunftsweisende Ausspruch, daß die Beziehungen zwischen Berechnung und Logik im vor uns liegenden Jahrhundert ebenso fruchtbar für die Entwicklung von Wissenschaft und Technik sein wird, wie dies im vergangenen Jahrhundert die Beziehung zwischen Analysis und Physik gewesen ist.

Geschichte der Logik