Anwendungsgebiete von LISP

 

Einleitung

Jede Programmiersprache hat ihre bevorzugten Anwendungsgebiete und wird auf eine gewisse Art von diesen charakterisiert. Das gilt trotz der Existenz sogennanter allgemeiner Programmiersprachen (general purpose programming languages) wie Pascal, PL/I und Ada. Zwar soll man mit diesen alle Probleme programmieren können, aber in Wirklichkeit werden entweder weite Anwendungsbereiche ausgespart oder mit Hilfe von Sprachdialekten bedient (PL/S für Systemprogrammierung usw.). Die interessante Wechselwirkung von Sprachenwurf (in Report), praktische Implementierung und wirklichem Nutzerkreis (bzw. Nutzerverhalten) ist hier zu beachten.

Obwohl LISP ebenfalls eine allgemeine Programmiersprache ist, wird sie doch bevorzugt für Probleme der nichtnumerischen Informationsverarbeitung eingesetzt. In diesem Anwendungsbereich wiederum haben neuere Programmiersprachen Bereiche abgedeckt, die mit LISP nicht ganz so natürlich zu behandeln sind wie mit ihnen. Man denke etwa an Probleme der Text- und Fileverarbeitung.

Auf dem ureigensten Anwendungsgebiet, dem der Künstlichen Intelligenz, hält sich LISP mit derselben Hartnäckigkeit, mit der FORTRAN für numerische Probleme aktuell geblieben ist. In beiden Fällen werden die Sprachen immer mal wieder totgesagt bzw. es wird behauptet, daß neuentwickelte Sprachen sie ablösen sollen. Die Ursachen für das Überleben sind recht naheliegend: Der weite Nutzerkreis, die Menge an fertigen und laufenden Programmen und die geringe Qualitätsverbesserung, die die neuen Sprachen bieten. Kein Programmierer wird sich, ohne dazu gezwungen zu sein, in die endlosen Schwierigkeiten einer so komplizierten Umstellung einlassen, wie sie der Wechsel zu einer anderen Programmiersprache mit sich bringt.

Für denjenigen, der für ein abgegrenztes Anwendungsproblem eine Programmiersprache ausgewählt hat, muß das Bekanntwerden mit dem ganzen Spektrum der Anwendungen höchst interessant und informativ sein. Das Wissen darüber dringt oft aus dem fast geschlossenen Kreis der Liebhaber der betreffenden Sprache nicht hinaus. In unserem Beispiel muß man sich darüber hinaus überlegen, wieso LISP für gerade diese Probleme die Programmiersprache Nummer 1 geblieben ist.

Um möglichst eine geschlossene Darstellung der Anwendungsgebiete zu geben, haben wir Programme, die typisch sind für solch ein Gebiet, aber nicht in LISP geschrieben worden sind, nicht extra ausgeklammert. Dies trifft insbesondere für das Programm {\tx ELIZA} als auch für eine ganze Reihe von Theorembeweisern zu, die nach dem Resolutionsprinzip arbeiten. Wir glauben, daß dennoch die Charakterisierung des jeweiligen Wissenschaftsgebiets als typisches Anwendugsgebiet zu Recht besteht.

Seit dem Buch von Berkeley und Bobrow [BB64] ist keine Zusammenfassungvon Anwendungsfällen von LISP mehr erschienen. Ein Projekt von 1970 ließ Bobrow fallen. So kann es sein, daß wichtigeAnwendungsfälle nicht erwähnt werden, obwohl sie neue Anwendungsgebiete erschließen.

Zwei Gebiete wurden überhaupt nicht erfaßt: Das sind zum einen die theoretische Anwendung des LISP-Kalküls für die Beschreibung von Programmiersprachen und zum anderen LISP als Forschunsgegenstand. Während die neueren Beschreibungssprachen ihre LISP-Ähnlichkeit trotz ihrer Herkunft von McCarthys Ideen [MCC64]weitgehend abgelegt haben [WEG72b,LUK78], scheint es nicht angemessen,Arbeiten, die LISP zum Gegenstand haben (etwa [CAR76]) und sich LISPselbst dabei als Hilfsmittel bedienen, in einem Zusammenhang mit den übrigen ``echten'' Anwendungsgebieten zu erwähnen.

 

Verarbeitung natürlicher Sprache - Frage-Antwort-Systeme

 

Das Problem

Turing hatte 1947 [TU69] bei der Frage nach der Möglichkeit,Maschinen Intelligenz zu verleihen zu können, ein Gedankenexperiment diskutiert, in dem ein Schachspieler abwechselnd gegen einen Menschen und gegen eine schachspielende Maschine antritt, ohne seinen Partner zu sehen. Seiner Meinung nach wäre eine Situation möglich, in der es dem Schachspieler außerordentlich schwerfiele zu entscheiden, ob sein Gegner ein Mensch ist oder nicht.

Bei der Frage nach der Definition von Intelligenz und dem Problem, wie künstliche Intelligenz zu erreichen sei, hat man dieses Gedankenexperiment zu einer Zielvorstellung abgeändert: Gelänge es, ein Programm zu entwickeln, daß mit einem Menschen einen Dialog in natürlicher Sprache so führen könnte, daß dieser nicht in der Lage wäre zu entscheiden, ob er einen menschlichen Gesprächspartner hat oder sich mit einer Maschine unterhält, dann könne man diesem Programm künstlichen Intelligenz nicht absprechen [PAL75].

Auf Grund dieser Vorstellung und durch die historische Entwicklung, die dazu geführt hat, daß im Zusammenhang mit Frage-Antwort-Systemen wesentliche Probleme der Künstlichen Intelligenz gestellt und zu lösen versucht wurden, ist die Verarbeitung natürlicher Sprache zu einem zentralen Anliegen der Wissenschaft von der künstlichen Intelligenz (McCarthy gebraucht 1977die Bezeichnug ``cognology'' für den Wissenschaftszweig und ``artificial intelligence'' für das Ziel) geworden.

Die Erfolgsaussichten für Versuche, natürliche Sprache mit Rechnern zu verarbeiten, werden seit den negativen Erfahrungen mit der automatischen Sprachübersetzung sehr zurückhaltend beurteilt. 1964 mußte das vorläufige Scheitern der Bemühungen in dieser Richtung eingestanden werden [ALP66].

Weshalb ist die Verarbeitung der natürlichen Sprache ungleich komplizierter als die der modernen Programmiersprachen? Antwort auf dieser Frage finden wir bei einer Analyse der Unterschiede [LEH76]: ``Auffallende Besonderheiten der natürlichen Sprache, denen bei der Modellierung des Sprachverstehens Rechnung getragen werden muß, sind:

Da die wirkliche Welt nicht nur aus diskreten, scharf gegeneinander abgegrenzten Objekten besteht und überdies einer beständigen zeitlichen Veränderung unterliegt, spielen unscharfe Begriffe für das menschlichen Denken eine große Rolle, was sich auch in der ``Unschärfe'' der Bedeutung der Äußerungen einer brauchbaren Universalsprache niederschlagen muß.

Darüber hinaus ist die Tatsache, daß die natürliche Sprache historisch gewachsen und nicht (wie formale Sprachen) nach rationalen Gesichtspunkten konstruiert worden ist, mitverantwortlich dafür, daß eine bestimmte Gegebenheit meist auf verschiedene Weise beschrieben werden kann, und daß unvermeidlich Mehrdeutigkeiten in den unterschiedlichen sprachlichen Ebenen (Lexik, Syntax, Semantik) auftreten.

Von entscheidender Bedeutung für die Mühelosigkeit und das Tempo verbaler Kommunikation ist die normalerweise vorhandene Einbettung aller kommunikativer Akte in einen sprachlichen und situativen Kontext und damit die Abhängigkeit der intendierten Bedeutung jeder Äußerung von einer Sequenz vorausgegangener Äußerungen (dem Kontext), von der Kommunikationssituation (Ort, Zeit beteiligte Personen, konkrete Umgebung, Anlaß und Zweck der Äußerung) und von der Gesamtheit des vom Sprecher bei der angesprochenen Person vorausgesetzten Vorwissens.

Ein außerordentlich wirkungsvolles Potential, das wesentlich zu der erstaunlichen Anpassungsfähigkeit der natürlichen Sprache an beliebige Gegenstandsbereiche beiträgt, liegt in den Möglichkeiten der elliptischen Verkürzung (zur Minimierung des erforderlichen deskriptiven Aufwandes) und des metaphorischen Sprachgebrauches (wobei das Verständnis der intendierten Bedeutung gewisser, in einem gewohnten Kontext auftretender Äußerungen an den Vollzug von Analogieschlüssen gebunden ist).

Die genannten Eigenschaften führen zu einem äußerst flexiblen und situationsbedingt ökonomischen Einsatz sprachlicher Mittel bei hoher Fehlertoleranz, d. h., ein gewünschter kommunikativer Effekt kommt zumeist trotz mehrfacher Verstöße gegen sprachliche Regeln noch zustande...''

Üblicherweise teilt man die Schritte bei der Sprachverarbeitung auf in lexikalische Analyse, Syntaxanalyse und semantische Interpretation. Während der lexikalischen Analyse werden z.B. Wortformen auf eine Grundform zurückgeführt, mit den im Lexikon aufgeführten Eintragungen verglichen und mit einem Repräsentanten identifiziert. Dabei wird versucht, das Wort in passende Klassen einzugliedern (Verb, Präposition u. ä.). Die Syntaxanalyse versucht, den Satz in seine grammatische Struktur zu zerlegen; üblicherweise wird dabei ein Zerlegungsbaum erzeugt. Die dabei zu befolgenden Regeln sind durch die Grammatik festgelegt. Im Zusammenhang mit der Analyse von Programmiersprachen ist viel über dieses Problem gearbeitet worden; die Verarbeitung natürlicher Sprache erfordert auf Grund der möglichen Mehrdeutigkeiten erweiterte Analysemethoden. Bei der semantischen Interpretation wird der Zerlegungsbaum in eine interne Zielsprache übersetzt. Diese interne Repräsentation ist wesentlich pragmatisch bestimmt: Was soll das Programm zum Sprachverstehen mit den Eingabesätzen anfangen? Im typischen Fall soll eine Eingabe mit der Datenbasis von Fakten in Beziehung gesetzt werden. Deshalb wird eine innere Struktur so ausgewählt, daß sie einerseits der natürlichen Sprache nahekommt und andererseits die Arbeit mit der Datenbasis erleichtert (Einspeichern, Rückgewinnen, Deduzieren).

Die meisten implementierten Systeme zur Verarbeitung natürlicher Sprache benutzen für die innere Repräsentation eine Mischung von Ideen aus Bereichen der Logik, Linguistik und Programmierung: Pädikatenkalkül, Graphen bzw. Netze linguistischer Tiefenstrukturen und Listenverarbeitung (LISP mit Listen, Graphen und Eigenschaftslisten).

Der wesentliche Fortschritt gegenüber den Arbeiten auf dem Gebiet der Sprachübersetzung besteht darin, daß man heute die Prozesse bei der Eingabeverarbeitung nicht in die angegebenen drei Aufgaben isoliert unterteilt. Zunächst hatte bei der maschinellen Übersetzung (engl. machine translation) lediglich der lexikalische Aspekt eine Rolle gespielt; später trat die Berücksichtigung der syntaktischen Struktur hinzu. Semantische oder gar pragmatische Analyseschritte wurden nie richtig einbezogen. Gegenwärtig ist man sich bewußt, daß schon Entscheidungen der lexikalischen Analyse durch kontextbezogene semantische Überlegungen gesteuert werden müßten. Die erforderliche Verflechtung der Teilprozesse bereitet damit große methodische Schwierigkeiten, denn der modulare Programmaufbau ermöglicht die programmtechnische Beherrschung der Analyseverfahren.

Es ist hier nicht möglich, auf die einzelnen Probleme weiter einzugehen. Der Leser wird auf die Literatur (Überblicksartikel [PAL75, LEH76, SIMM 65, SIMM70], Sammelbände mit neueren Resultaten[BO75, AD75,SCHA73, WINO72]) verwiesen.

Als wesentliches Problem hat sich immer mehr die Frage nach der passenden Wissensrepräsentation (Aufbau und ? der Datenbasis) erwiesen. Die Auswirkung einer angemessenen Entscheidung auf diesem Gebiet auf das gesamte Verarbeitungssystem sind enorm, hängen doch sowohl Eingabeanalyse als auch Such- und Ableitungsprozesse von ihm ab. Die wichtigsten Ideen dafür stehen natürlich in engstem Zusammenhang mit der internen Sachrepräsentation; hier dominiert gegenwärtig das Paradigma der semantischen Netze [QI68], während sich die Vorschlägezur Wissendarstellung durch Prozeduren [WOO68] oder durch Mengen voneinfachen prädikatenlogischen Formeln (sogenannten Klauseln, vgl. [GCR69a, 69b, KOW74]) als weniger angemessen erwiesen haben.

 

Überblick über die Fähigkeiten einiger realisierter Systeme

1965 beschrieb Simmons[SIMM65] acht Systeme zur Verarbeitungnatürlicher Sprache. Unter diesem nahmen die Programme {\tx BASEBALL} [GRB6], {\tx STUDENT} [BO63b], {\tx SADSAM} [LIN63] und {\tx SIR}[RA63] einen besonderenPlatz ein.

{\tx BASEBALL} beantwortete verschiedenste englischsprachige Anfragen über Ort, Zeit, beteiligte Mannschaften und Ergebnisse aller während einer Saison stattgefundenen Baseballspiele in den USA.

{\tx STUDENT} löste einfache Textaufgaben im Oberschulniveau, wie z.B.: ``Wenn die Zahl der Kunden vom Tom das Doppelte des Quadrats von 20 Prozent der Zahl der Reklameannoncen ist, die er aufgibt, wieviele Kunden hat dann Tom, wenn er 45 Annoncen aufgibt?''

{\tx SADSAM} bestimmte Verwandtschaftsverhältnisse zwischen Personen aus einem Kreis untereinander verwandter Menschen.

{\tx SIR} beantwortete Fragen über Relationen zwischen Objekten. Gab man z.B. ein:

Eine Nase ist Teil einer Person. Ein Nasenloch ist Teil einer Nase. Ein Professor ist ein Lehrer. Ein Lehrer ist eine Person. </plaintext>so konnte man anschließend fragen: {\tt Ist ein Nasenloch Teil eines Profes}<font COLOR="00FF00">sors?</font>, und das System antwortete: <font COLOR="00FF00">Ja</font>\footnote{Natürlich auf Englisch!}</p> <p>Diese Systeme der ersten Generation hatten große Bedeutung für die Ermutigung der Forscher nach dem Zusammenbruch der Hoffnungen bezüglich der Sprachübersetzung. Sie beruhten auf geschickter Kombination von Ad-hoc-Techniken für linguistische Analyse und einfachen Dastellungsmodellen; {\tx STUDENT} und {\tx SIR} waren in LISP programmiert. </p> <p>Daß man mit recht einfachen Mitteln überraschende Resultate erzielen kann, bewies 1964 das System {\tx ELIZA} [WEI66]\footnote{{\tx ELIZA}war nicht in LISP, sondern in SLIP programmiert.}. Dieses Programm führte keine vollständige Analyse der Eingabesätze aus, sondern versuchte, sie mit Grundmustern zu vergleichen. Ließ sich im Musterrepertoire ein passendes finden, dann antwortete {\tx ELIZA} mit einer abgeleiteten einfachen Transformation des Eingabesatzes. Gab es kein entsprechendes Muster, dann benutzte {\tx ELIZA} leere Floskeln oder ging auf frühere Themen zurück. </p> <p>Die mit diesen recht unseriös scheinenden Methode erzielten Ergebnisse konnten so manchen Uneingeweihten überraschen. <font COLOR="0000FF">Palme</font>[PAL75] berichtet über eine Art <font COLOR="0000FF">Turing</font>-Test, den {\tx ELIZA} bestand: Ein Vertreter wollte ein Betriebssystem vorführen. Bei der Suche nach einer passenden Möglichkeit fand er ein Terminal, auf dem der Hinweis angebracht war: ``Reserviert für Prof. Bobrow''. Er schrieb nun über den Fernschreiber Prof. Bobrow an, mit dem er glaubte verbunden zu sein, um sich über freie Rechnerkapazität zu erkundigen. In Wirklichkeit aber war er mit {\tx ELIZA} verbunden (vermutlich hatte Bobrow mit {\tx ELIZA} gearbeitet und war kurzfristig aus dem Raum gegangen). Es entwickelte sich folgender Dialog ([PAL75], S. 211):</p> <p>\vspace{5mm} </p> <p>\begin{tabular}{ll} Vertreter: &amp; <font COLOR="00FF00"> Denken Sie, daß ich heute morgen den Rechner benutzen</font>\\&amp; <font COLOR="00FF00">kann?</font>\\{\tx ELIZA}: &amp; <font COLOR="00FF00">Warum fragen Sie?</font>\\Vertreter: &amp; <font COLOR="00FF00">Ich könnte einige zusätzliche TELECOMP-Verkäufe ma-</font>\\&amp; <font COLOR="00FF00">chen.</font>\\{\tx ELIZA}: &amp; <font COLOR="00FF00">Warum sind sie nicht sicher?</font>\\Vertreter: &amp; <font COLOR="00FF00">Meine möglichen Käufer haben noch nie eine Vorführung</font>\\&amp; <font COLOR="00FF00">des Systems gesehen.</font>\\{\tx ELIZA}: &amp; <font COLOR="00FF00">Bedeutet das denn viel für Sie?</font>\\Vertreter: &amp; <font COLOR="00FF00">Aber ja!</font>\\{\tx ELIZA}: &amp; <font COLOR="00FF00">Sie scheinen sich Ihrer Sache aber sehr sicher zu</font>\\&amp; <font COLOR="00FF00">sein!</font>\\Vertreter: &amp; <font COLOR="00FF00">Sie verspotten mich!</font>\\{\tx ELIZA}: &amp; <font COLOR="00FF00">Warum glauben Sie, daß ich Sie verspotte?</font>\\Vertreter: &amp; <font COLOR="00FF00">Gibt es nun irgendeinen Grund, warum ich den Rechner</font>\\&amp; <font COLOR="00FF00">jetzt nicht benutzen kann?</font>\\{\tx ELIZA}: &amp; <font COLOR="00FF00">Erzählen Sie mir mehr über Ihre wahrscheinlichen</font>\\&amp; <font COLOR="00FF00">Käufer!</font>\\Vertreter: &amp; <font COLOR="00FF00">Bitte rufen Sie mich unter 491-1850 an!</font>\\\end{tabular} </p> <p>Hier brach der Vertreter den Dialog ab, weil ihm das Medium unbequem wurde und es ist reizvoll sich vorzustellen, daß Bobrow wiederkam und alle Beteiligten in ein großes Gelächter ausbrachen. </p> <p>Obwohl das zugrunde liegende Prinzip keinen schöpferischen Beitrag zur Fortentwicklung der Verarbeitung natürlicher Sprache geleistet hat, darf man {\tx ELIZA} auch nicht als bloßen Unsinn abtun. <font COLOR="0000FF">Shapiro</font> und<font COLOR="0000FF">Kwasny</font> [SHA75] haben versucht, die Ideen von <font COLOR="0000FF"> Weizenbaum</font> in einenseriöseren System anzuwenden. Die hauptsächliche Bedeutung des Systems {\tx ELIZA} liegt aber darin, daß in der Sprachverarbeitung deutlich wurde, daß wohltönende, in ihrer Logik kaum begründete Phrasen, die in einem losen Zusammenhang mit den Problemen eines Gesprächspartners stehen, kaum daneben treffen. Auf ähnliche Weise kommt der Erfolg der Wahrsager, Orakel aber auch der Pseudowissenschaft zustande. Man erinnere sich auch an die vielsagend hintergründigen Antworten in den Frage-Antwort-Spielen, die gut gemischten Karten produzieren können. </p> <p>{\tx ELIZA} zeigt außerdem deutlich die Fragwürdigkeit und Unbrauchbarkeit des sogenannten <font COLOR="0000FF">Turing</font>-Tests. So erweist sich dieKünstliche Intelligenz als eine von den Wissenschaften mit einem zwar intuitiv recht klaren Ziel, das bisher aber weder hinreichend präzise formuliert noch zu einem exakten Kriterium entwickelt werden konnte. </p> <p>Die Systeme der zweiten Generation aus den frühen siebziger Jahren zeigten einen wichtigen Schritt nach vorn. Die linguistischen Verarbeitungskapazitäten hatten sich wesentlich weiterentwickelt, die Eingabesätze durften eine ziemlich komplizierte Struktur haben. Daneben waren teilweise größere Möglichkeiten zum Ziehen von Schlußfolgerungen vorhanden. Beispiele für diese Systeme sind {\tx LUNAR} [WOO72], {\tx SHRDLU}, [WINO71],{\tx MARGIE} [GOLM73] und {\tx SQAP} [SAN71].</p> <p>{\tx LUNAR} war gedacht für die Beantwortung von Fragen über die Mineralproben, die vom Mond stammen. Es gab eine große Datenbasis, die beschrieb, wo jede Probe aufgelesen war, welche Untersuchungen mit ihr ausgeführt worden waren, welches ihre Bestandteile waren usw. Man konnte nun in natürlicher Sprache konkrete Fragen über die Proben stellen, wie z.B.: </p> <p><font COLOR="00FF00">Was ist die durchschnittliche Aluminiumkonzentration in den hoch-alkalischen Steinen?</font></p> <p>oder: </p> <p><font COLOR="00FF00">Wieviele Bruchstücke enthalten Olivin?</font></p> <p>usw. usf. </p> <p>{\tx SHRDLU} verstand Fragen und Anweisungen, die sich auf Bauklötze bezogen, die auf einer Tischplatte verteilt waren. Das System war mit einem Manipulator gekoppelt, der die Anweisungen ausführte. Ein typisches Beispiel für einen Dialog mit {\tx SHRDLU} ist etwa [WINO74][S. 21ff]:</p> <p>\begin{tabular}{ll} $\rightarrow$ &amp; <font COLOR="00FF00"> Nimm einen großen roten Block.</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">OK.</font>\\$\rightarrow$ &amp; <font COLOR="00FF00">Nimm die Pyramide</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">Ich weiß nicht, welche Pyramide du meinst.</font>\\$\rightarrow$ &amp; <font COLOR="00FF00">Finde einen Block, der schmaler ist als der, den du in der</font>\\&amp; <font COLOR="00FF00">Hand hältst, und tue ihn in den Kasten.</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">OK.</font>\\$\rightarrow$ &amp; <font COLOR="00FF00">Was ist in dem Kasten?</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">Die blaue Pyramide und der blaue Block.</font>\\$\rightarrow$ &amp; <font COLOR="00FF00">Was liegt unter der Pyramide?</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">Der Kasten.</font>\\$\rightarrow$ &amp; <font COLOR="00FF00">Wieviele Blöcke liegen nicht im Kasten?</font>\$\leftarrow$ &amp; <font COLOR="00FF00">Vier von ihnen.</font>\\\end{tabular} </p> <p>usw. usf. </p> <p>{\tx MARGIE} zeigte eine Art Verstehen, indem es eine Eingabe auf verschiedenste Art formuliert wieder ausgab oder indem es einfache Schlüsse zog: </p> <p>\begin{tabular}{ll} $\rightarrow$ &amp; <font COLOR="00FF00"> John gab Mary etwas Aspirin,</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">John glaubte, daß Mary Aspirin möchte.</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">Mary ist unwohl.</font>\\\end{tabular} </p> <p><font COLOR="00FF00">SQAP</font> basierte in seiner ersten Version auf einemvereinfachten Englisch, mit dem man fast alle genauso präzise wie in natürlichen Englisch ausdrücken konnte; dabei waren aber schwer übersetzbare Teile oder mehrdeutige Elemente eliminiert worden. Die syntaktischen Haupteinschränkungen waren [PAL75][S.252]: Alle Verbenmußten in Partizip- oder in Passivform vorliegen, mehrdeutige Präpositionen waren ausgeschlossen, relativische Pronomina mußten Subjekte sein, und mehrdeutige Konjunktionen mußten mit Klammern aufgelöst sein. </p> <p>Seit etwa 1973 hat sich die Forschung stark aufgesplittert -- man versucht, Teilprobleme zu lösen. Es ist jedoch bekannt, daß z.B. bei der Firma XEROX an einem integrierten System zur Büroautomatisierung auf der Basis natürlicher Sprache gearbeitet wird. </p> <p>Einen gewissen Eindruck von dem erreichten Stand von 1979 vermittelt das Sprachverstehenssystem {\tx SAM} [SCHA75a], eine Weiterentwicklung von {\tx MARGIE}. Um einen Kontext zu haben, wird vor dem eigentlichen Dialog eine Geschichte eingegeben, aus der eine Datenstruktur aufgebaut wird, der <font COLOR="FF0000">Skript</font>. Neue Eingaben werden in den Skript eingebaut;bei Fragen wird der angepaßte Skript identifiziert und dann unter Verwendung von Schlußfolgerungen, die entlang Kausalverknüpfungen vorgehen, beantwortet. Außerdem wird etwa in der Art, wie dies {\tx MARGIE} tat, eine Art Pharaphrase produziert. Folgendes Beispiel aus dem Jahre 1975 ist recht eindrucksvoll [SCHA75B]: </p> <p>\vspace{0.5mm} </p> <p>Eingabe: {\tt John ging in eine Gaststätte. Die Kellnerin wies ihm ei- nen Platz an. Die Kellnerin gab John eine Speisekarte. Der Ober \\ kam zum Tisch. John bestellte Hummer. John wurde schnell bedient. \\ John gab ein großes Trinkgeld. John verließ die Gaststätte.} </p> <p>\vspace{0.5mm} </p> <p>Ein darauffolgender Dialog: </p> <p>\vspace{0.5mm} \begin{tabular}{ll} $\leftarrow$ &amp; <font COLOR="00FF00">Was aß John?</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">Hummer.</font>\\$\rightarrow$ &amp; <font COLOR="00FF00">Wer gab John die Speisekarte?</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">Die Kellnerin.</font>\\$\rightarrow$ &amp; <font COLOR="00FF00">Wer gab John den Hummer?</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">Wahrscheinlich der Ober.</font>\\$\rightarrow$ &amp; <font COLOR="00FF00">Wer bezahlte die Rechnung?</font>\\$\leftarrow$ &amp; <font COLOR="00FF00">Wahrscheinlich John.</font>\\\end{tabular} </p> <p>usw. </p> <p>\vspace{0.5mm} </p> <p>Paraphrase: {\tt John entschied sich, daß er in eine Gaststätte gehen\\ sollte. John ging in eine Gaststätte. John sagte der Kellnerin,\\ daß er gerne einen Tisch haben möchte. Die Kellnerin bedeutete\\ John, er könne zu einem Tisch gehen. John setzte sich auf den\\ Stuhl. John bekam die Speisekarte. Der Ober sah, daß John am Tisch saß. Der Ober kam zum Tisch. John bestellte Hummer. Der Küchenchef richtete den Hummer zu. Der Ober bekam den Hummer vom Küchenchef.\\ Der Ober servierte John den Hummer. John aß den Hummer. John zeig-\\ te dem Ober, daß er gerne die Rechnung hätte. John bekam die Rech- nung vom Ober. John gab dem Ober ein großes Trinkgeld. John be-\\ zahlte die Rechnung. John verließ das Restaurant.} </p> <p>\vspace{0.5mm} </p> <p>Zusammenfassung: <font COLOR="00FF00">John ging in eine Gaststätte und aß Hummer.</font>\footnote{Bei diesem und anderen Beispielen handelt es sich um möglichst getreu ins Deutsche übersetzte englische Dialoge.} </p> <p>Im Zusammenhang mit diesem und mit allen anderen erwähnten Systemen darf nicht unerwähnt bleiben, daß es sich vorerst um experimentelle Systeme zu Forschungszwecken handelte, die fast ausnahmslos nur von der Gruppe benutzt wurden, von der sie jeweils entwickelt wurden. Daher ist es recht schwierig, objektiv zu beschreiben oder gar zu bewerten, welchen Sprachbereich diese Systeme überdecken und welchen Restriktionen sie unterliegen. Für einen wirklich praktischen Einsatz erscheinen die bisher vorhandenen Methoden trotz der offenkundigen Fortschritte noch nicht genügend ausgereift. </p> <p>In den umfänglichen und hochgestochenen (allerdings ebenfalls experimentellen) Systemen für das Verstehen gesprochner natürlicher Sprache wie <font COLOR="00FF00"> SPEECHLIS</font> [WOO75], <font COLOR="00FF00">HEARSAY II</font> [LES75], {\tt HWIM} [WOO76], <font COLOR="00FF00">HAPPY</font> [LOW76] und <font COLOR="00FF00">SRI-SDC</font> [WALK75]kulminiert derzeit die Wissenschaft von der Verarbeitung natürlicher Sprache. Obwohl die komplexen Probleme bei der phonetischen Erkennung gesprochener Sprache zu denen bei der semantischen Analyse hinzukommen, scheint man durch klug gewählte Einschränkungen einige Erfolge erzielen zu können. Allerding zeigte sich, daß die gegenwärtige Hardware den Ansprüchen bezüglich Geschwindigkeit und anderer technischer Parameter noch nicht gewachsen ist, die man im Zusammenhang mit dem Sprachverstehen stellen muß. </p> <p>&nbsp;</p> <h2>Beweis logischer Theoreme</h2> <p>&nbsp;</p> <h3>Das Problem</h3> <p>In einem Frage-Antwort-System tritt häufig die Situation auf, daß eine Frage gestellt wird, deren Antwort nicht durch bloßes Suchen in der Datenbasis gefunden werden kann. Es sind Deduktionsschritte nötig, um aus gegebenen Fakten und eventuell verfügbaren allgemeinen Sätzen solch einen unbekannten Tatbestand aufzuklären. Auf Grund der ... Wissenrepräsentation im Frage-Antwort-System kann die dazu erforderliche Deduktion von ... verschiedener Komplexität sein. </p> <p>Wenn wir an das im Abschnitt 2.2 erwähnte Beispiel für das System {\tx SIR} anknüpfen, können wir es nun als Beispiel einer Deduktion interpretieren: </p> <p>Die Frage: <font COLOR="00FF00">Ist ein Nasenloch Teil eines Professors?</font> wirdbeantwortet, indem nach einer Deduktion für den Satz: {\tt Ein Nasenloch ist ein Teil eines Professors.} aus der Datenbasis: </p> <p><font COLOR="00FF00"><plaintext>Eine Nasenloch ist Teil einer Person; Ein Nasenloch ist Teil einer Nase; Ein Professor ist ein Lehrer; Ein Lehrer ist eine Person; </plaintext></p> <p>gesucht wird. </p> <p>Die <font COLOR="FF0000">Relationen</font> zwischen den Objekten (Nase, Person, usw.) können in der Datenbasis so abgespeichert sein, daß die Deduktion durch <font COLOR="FF0000">Verfolgung der Relationsverbindungen</font> fortschreiten kann: Man beginnt z.B. beim Nasenloch und fragt nachverfügbaren Relationen. Um zu der Aussage ist Teil von zu kommen,darf bei der Verfolgung der Relationsketten nur auf Eigenschaften von der Art ist Teil von bzw. ist ein (entspricht der Element- bzw.Teilmengenrelation) geachtet werden. Die Deduktion läuft umso schneller ab, je direkter sie vom Nasenloch zum Professor gelangt, d.h. jeweniger Teilmengenrelationen berücksichtigt werden müssen. Bei der Suche nach der jeweils nächsten passenden Relationsverbindung bevorzugt das Deduktionsprogramm also die Relation ist-Teil-von.</p> <p>In diesen praktischen Beispiel ist der Ablauf der Deduktion unmittelbar klar. Man sieht leicht ein, daß bei einem derartigen Vorgehen die Relationen bestimmte Eigenschaften haben müssen: Sie müssen transitiv und untereinander verträglich sein usw. Man wird jedoch erwarten, daß man auf diese Weise nicht oft vorgehen kann. </p> <p>Diese Art der Deduktionsprozedur heißt <font COLOR="FF0000"> positiv</font>, weil vonder Datenbasis zum Fragesatz eine Deduktionskette aufgebaut wird ([PAL75], S.237). Die Antwort auf die Frage ist Ja, wenn eine solche Kette gefunden wird, und Nein, wenn eine solche Kette zur Negation der Frage aufgebaut werden kann. </p> <p>Positive Deduktion muß nicht nur in der Konstruktion von Relationsketten bestehen. <font COLOR="0000FF">Sandewall</font> [SAN69a, b] entwickeltfür ein Frage-Antwort-System solche Methoden systematisch. </p> <p>Eine grundsätzlich andere Möglichkeit, Deduktionen mit einer Datenbasis vorzunehmen, besteht in dem Versuch, aus der um die betreffende Frage erweiterten Datenbasis einen Widerspruch abzuleiten (<font COLOR="FF0000">negative</font> Deduktion). Hier wird also eine Deduktionskette zueinen negativen Resultat gesucht: Kann der Widerspruch abgeleitet werden, so ist die Antwort Nein, Kann der Widerspruch abgeleitetwerden, wenn statt der Frage ihre Verneinung (Negation) aufgenommen wird, heißt die Antwort Ja.</p> <p>Da die Prädikatenlogik oft als wesentliche Grundlage für die interne Repräsentation der Datenbasen benutzt wurde, ist es möglich, die Deduktionsprozeduren unabhängig von konkreten Frage-Antwort-Systemen zu entwickeln. </p> <p>Neben der Anwendung der Frage-Antwort-Systeme tauchen ähnliche Probleme immer dort auf, wo eine Datenbasis mit neuen Fakten konfrontiert wird: Bei der Robotersteurung, beim Lösen von Problemen usw. Außerdem gibt es Gebiete der nichtnumerischen Informationsverarbeitung, wo direkt logische Theoreme generiert werden und Aufmerksamkeit verdienen. Ein sehr anschauliches Beispiel ist die <font COLOR="FF0000"> Programmverifikation</font> (Abschnitt 2.5).</p> <p>Schließlich kann man das Problem, Beweise für gegebene Sätze in einer mathematischen Theorie zu finden, für sich betrachten. In derselben Weise, wie die Programmentwicklung erleichtert, automatisiert und vom Rechner unterstützt wird, kann auch die Beweisführung unterstützt werden. Insofern tritt das Problem, Theoreme in einer formalen Sprache zu beweisen, als selbstständige Aufgabe an der Forschung heran. Durch die Formalisierung werden die Aspekte der natürlichen Sprachen abgetrennt; die Produkte der Formalisierung, die Formeln, lassen sich durch rein syntaktische Umformungen manipulieren. </p> <p>Von allen Teilgebieten der nichtnumerischen Informationsverarbeitung überlagert sich das Theorembeweisen mit der am meisten ausgearbeiteten Theorie des Gegenstandsbereichs. Schon vor der Zeit, da man sich über die Verwendung von Rechnern für das Beweisen logischer Theoreme Gedanken machte (seit etwa 1956 ist das der Fall), hat sich die Logik mit Beweisverfahren beschäftigt. Die dabei erzielten Resultate gehören zu den wichtigsten der Logik überhaupt; für die Möglichkeit bzw. Unmöglichkeit der Automatisierung mittels Maschinen spielen sie die entscheidende Rolle. </p> <p>Eine der zentralen Fragen der Logik, die in Bezug auf einen formalen Kalkül, das heißt, eine Kombination aus formaler Sprache (zur Notation von Formeln) und einer Menge von Ableitungsregeln, gestellt werden, ist die Frage nach der Existenz eines <font COLOR="FF0000">Entscheidungsverfahrens</font>. Ein solches Verfahren ist einallgemeiner Algorithmus, der für ein formales System zu jeder vorgelegten Formel in endlich vielen Schritten entscheidet, ob sie allgemeingültig ist oder nicht (der Leser konsultiere zu den benutzten Begriffen ein Lehrbuch der formalen Logik, etwa [ASS72]).</p> <p>Die Entscheidbarkeit (d.h. die Existenz eines Entscheidungsverfahrens) des Aussagenkalküls, also des formalen Systems, in dem Aussagen als Grundeinheiten betrachtet und nur ihre Verknüpfungen formalisiert werden, wurde 1921 durch <font COLOR="0000FF">Emil Post</font>bewiesen. Für den Prädikatenkalkül 1. Stufe, d.h. für das formale System, das auch Relationen zwischen den Variablen formalisiert und in dem zu den logischen Verknüpfungen Quantifizierungen hinzu genommen sind (``für alle'', ``es gibt ein''), konnte erst 1936 von {\sc Alonzo Church} nachgewiesen werden, daß es kein Entscheidungsverfahren werden kann. </p> <p>Damit sind der Automatisierung des Beweisens enge Grenzen gesetzt: Man kann zwar für jedes Theorem zeigen, daß es ein Theorem ist, jedoch für andere Aussagen (Formeln) kann es vorkommen, daß das Verfahren nicht abbricht. Das Unangenehme an der Situation ist, daß man keine obere Schranke für den zum Finden des positiven Resultats erforderlichen Aufwand angeben kann: In der Praxis wird man Beweisversuche abbrechen müssen, ohne zu wissen, ob für diesen Fall die Zeit nicht reichte oder ob ein prinzipielles Nichtterminieren vorliegt. </p> <p>Man sagt, um diese Situation zu charakterisieren, daß der Prädikatenkalkül erster Stufe <font COLOR="FF0000"> semi-entscheidbar</font> sei und daß man kein Entscheidungsverfahren aufstellen könne, sondern nur ein Beweisverfahren. </p> <p>&nbsp;</p> <h3>Das Resolutionsverfahren als oft benutztes Beweisverfahren</h3> <p>Trotz der negativen Resultate haben sich Logiker weiter mit der ``Mechanisierung'' der Beweise in Prädikatenkalkül beschäftigt [BET55,HIN55,KAN57,SCHU54], und als man etwa 1957 mit derImplementierung beweisender Programme begann, konnte man ihre Ergebnisse verwenden. <font COLOR="0000FF">D. Prawitz</font> [PRAW60] dürfte 1957 der erste gewesensein, der ein solches Programm aufstellte. Anfang 1960 gab es schon eine ganze Reihe von Theorembeweisern. Die Möglichkeiten dieser Systeme waren auf Grund ihrer Eigenschaft, gewisse Ausdrucksmengen erschöpfend zu generieren bzw. abzusuchen, begrenzt. Ein entscheidender Durchbruch gelang <font COLOR="0000FF"> J.A.Robinson</font> etwa 1963 [ROB65] mit der Formulierung des<font COLOR="FF0000">Resolutionsprinzips</font>. </p> <p>In einem Programm, das nach diesem Prinzip arbeitet, wird versucht, aus der Verknüpfung der zur Debatte stehenden Formel und den Axiomen (Fakten der Datenmenge, Axiome einer Theorie usw.) einen Widerspruch abzuleiten, d.h. das gleichzeitige Auftreten eines Prädikats und seiner Negation für gleiche Argumente nachzuweisen -- das heißt, das Resolutionsverfahren ist ein {\bf Widerlegungsverfahren}. Dieser Widerspruch wird erzeugt, indem gezielt nach Instanziierungen der Teilformeln gesucht wird, um diesen Widerspruch zu etablieren. </p> <p>Zunächst wird aus der Konjuktion (``und''-Verknüpfung) von Formeln und Axiomen eine <font COLOR="FF0000">Normalform</font> abgeleitet. Dabei werden dielogischen Verknüpfungen durch äquivalente Verknüpfungen mittels ``nicht'', ``und'' und ``oder'' ersetzt. Die zu beachtenden Regeln ähneln den Ausklammerungsregeln der Arithmetik (``ausdistributieren''). Die Normalform zeigt dann eine hinreichend hierarchische Form bezüglich des Auftretens der logischen Operatoren. </p> <p>Die Grundbestandteile der Normalform sind die <font COLOR="FF0000">Atome</font>, d.h.prädikative Ausdrücke, wie z.B.: GRÖSSER(X,F(Y)).</p> <p>Nimmt man als einstellige Verknüpfung die Negation hinzu, so bekommt man die Klasse der <font COLOR="FF0000">Literale</font>: NICHT GRÖSSER(Y,X), KLEINER(Z,G(X))\footnote{Statt NICHT GRÖSSER(Y,X) wird $\neg$ GRÖSSER(Y,X)notiert.} usw. </p> <p>Die Normalform selbst ist eine {\em Konjunktion von Disjunktionen von Literalen}, also beispielweise {\tt ($L_{1}$ ODER $L_{2}$ $...$ ODER $L_{i}$) UND ($L_{i+1}$ ODER $...$ ODER $L_{j}$)} {\tt UND $...$ UND ($L_{k}$ ODER $...$ ODER $L_{n}$)}.\footnote{Statt ODER} schreibt man $\vee$, statt UND $\wedge$.</p> <p>Dabei sind etwa auftretende Quantoren zunächst an den Anfang der Formel geschoben worden (<font COLOR="FF0000">Pränex-Normalform)</font>. Anschließend wurden nacheinem von <font COLOR="0000FF">Skolem</font> erdachten Verfahren (<font COLOR="FF0000">Skolemisieren</font>) die Existenz-Quantorenentfernt und die All-Quantoren weggelassen (zu diesem Zeitpunkt gab es nur noch diese Art von Quantoren). In dieser <font COLOR="0000FF">Skolem</font>-schen konjuktiven Normalform versteht sich die Stellung der Junktoren von selbst, und deshalb läßt man auch sie meist weg. Da Konjunktion und Disjunktion kommutativ, assoziativ und idempotent sind, spielen Reihenfolgen und mehrfaches Auftreten keine Rolle und man kann die Formelglieder jeweils als Mengenelemente betrachten. Das Resolutionsverfahren arbeitet also mit einer Menge (der konjuktiven Normalform) von konjunktiv verknüpften Klauseln (Disjunktionen), die ihrerseits Mengen von disjunktiv vernüpften Literalen sind. </p> <p>Auf diese <font COLOR="FF0000">Klauselmenge</font> wird nun schrittweise die Resolutionsregel angewandt.Dabei versucht man, passende Klauseln <font COLOR="FF0000">auszuwählen</font>, in denen <font COLOR="FF0000">verwandte</font> Literale auftreten und aus ihnen unter Herausschneiden der ausgewählten Literale eine neue, möglichst kürzere Klausel (die sogennante Resolvente) zu bilden. Vereinfacht dargestellt, sucht man etwa eine Klausel, in der ein bestimmtes Literal steht, und eine zweite, in der das nämliche Literal, nur negiert, auftaucht. Die Resolvente besteht aus der Vereinigung beider Klauseln unter Fortlassen des jeweiligen ausgewählten Literals. </p> <p>\vspace{3mm} </p> <p>\noindent Klausel1: {\tt ($A_{1}, A_{2}, A_{3}, A_{4}$)}\\ Klausel2: {\tt (-$A_{2}, A_{5}, A_{6}, A_{7}$)}\\ ausgewählte Literale: {\tt $A_{2}$}; {\tt -$A_{2}$}, \\ Resolvente: {\tt ($A_{1}, A_{3}, A_{4}, A_{5}, A_{6}, A_{7}$)}. \\ </p> <p>Der <font COLOR="FF0000">Widerspruch</font> taucht auf, wenn schließlich zweiKlauseln gefunden werden, deren Resolvente <font COLOR="FF0000">leer</font> ist. Man siehtdies leicht, wenn man sich wieder der Vereinfachung bedient: Die Resolvente wird sicher leer sein, wenn eine Klausel nur aus einem unnegierten Literal vorliegt und dazu eine andere Klausel, die nur aus der Negation dieses Literals besteht. Die Existenz dieser beiden Klauseln bedeutet aber, daß das Literal und seine Negation durch ``und'' verknüpft sind. </p> <p>In dieser sehr knappen Beschreibung des Resolutionsverfahrens (für ausführliche Erläuterungen siehe etwa [ROB70,PIR74,BOT75]) zeigensich aber doch eine ganze Reihe von Problemen, die bei der wirklichen Implementation die Effizienz entscheidend beeinflussen: Die Klauseln sind auszuwählen, die Literale sind auszuwählen, die Verwandtschaft ist zu überprüfen, die Resolvente ist zu bilden. Für diese Teilprozesse sind Steuerungsverfahren (sogennante <font COLOR="FF0000">Strategien</font> -- man wählt etwa nur Klauseln mit passenden Literalen) entwickelt worden, die sich teilweise überschneiden und die die Resolutionsschritte merklich beeinflussen. Da meist Kombinationen verschiedener Strategien angewandt werden, gibt es leider bisher kaum Vergleiche über ihre Wirksamkeit im einzelnen (vgl. [MEL75,WILS76]).</p> <p>Ein besonderes Problem beim Beweis ist die Berücksichtigung der <font COLOR="FF0000">Gleichheit</font> als besonderes Prädikat. Einige der Axiome können etwa Gleichungen zwischen Termen sein. Wenn nun in einem Literal, das in einem Resolutionsschritt verwendet werden könnte, einer dieser Terme auftritt, dann versucht man, falls er sich für die Substitution nicht eignet, den Term auf der anderen Seite der Gleichung an seiner Stelle zu verwenden[ROBG69].</p> <p>Die nach dem Resolutionsverfahren arbeitenden Beweiser haben erfolgreich ihre Bewährungsprobe bestanden. Die pessimistischen Äußerungen von <font COLOR="0000FF">Bledsoe</font> [BLE71], daß dieResolutionsbeweiser die Eigentümlichkeit besitzen, entweder einen Beweis extrem schnell zu finden oder aber überhaupt nicht, scheinen inzwischen etwas überholt [MCC76].</p> <p>Dennoch kann man eine grundlegende Tatsache feststellen: Das Resolutionsverfahren ist ein syntaktisches Verfahren, in dem </p> <ol> <li>die Bedeutungen weder der Axiome noch des zubeweisenden Satzes berücksichtig werden (einige Strategien erlauben die Bevorzugung von Klauseln auf Grund ihrer Herkunft bzw. gehen von einer Ordnung der Literale aus, die der Nutzer auf Grund semantischer Überlegungen vorgeben kann; auch Wahrheitswertteste in vorgegebenen Interpretation können durchgeführt werden (semantic resolution)\footnote{ In der Theorieresolution werden ...}), </li> <li>die Struktur der betroffenen Formel durch die Bildung der Normalform zerstört wird (es gibt allerdings Resolutionskalküle für komplexe Formeln) und </li> <li>Beweislinien verfolgt werden, die für den Menschen nichtunmittelbar klar sind. </li> </ol> <p>Ein ``natürlicheres'' Beweisverfahren hätte sich mehr an menschlichen Vorgehensweisen zu orientieren (der Mensch könnte Beweisschritte der Maschine einfacher verstehen und wäre in der Lage, Hilfestellung zu bieten) und müßte sowohl strukturelle als auch semantische Eigenschaften -- das heißt bereichs-spezifisches Fachwissen -- des Beweisproblems stärker berücksichtigen. </p> <p>&nbsp;</p> <h3>Natürliche Beweisverfahren </h3> <p>Schon das erste Programm der KI, das nicht eigentlich ein Theorembeweiser gewesen ist, obwohl es Theoreme im Aussagenkalkül bewies, bediente sich keiner rein syntaktischen Methoden, sondern war nach Methoden aufgebaut worden, deren sich Studenten der Logik beim Beweisen von Theoremen bedienen [NEW56]. Doch war die Zeit (und die Rechner) für derartige Experimentenicht reif. Bezüglich der Anwendungsbeispiele bezeichnete {\sc Wang} [WAN60] diese Vorgehensweise als mit ``Kanonen nach Spatzen zuschießen'' -- aber Zweck des Programms war die Demonstration der Technik, nicht die optimale Erfüllung einer Anwendungsaufgabe. </p> <p>Das erste eigentliche Beweisprogramm, das die schon 1956 entwickelten Ideen für heuristische Beweismethoden aufgriff, war ein von <font COLOR="0000FF">Bledsoe</font>[BLE72] für Beweise in der Mengenlehre aufgestelltes Programm. Dabeiwurde zunächst ein Resolution-Theorembeweiser mit Programmteilen zur <font COLOR="FF0000">Zerlegung</font> und <font COLOR="FF0000"> Vereinfachung</font> des zu beweisenden Theoremsumgeben. Die in übrigen Gebieten der Künstlichen Intelligenz erfolgreich benutzte Strategie, ein Problem in <font COLOR="FF0000"> Teilprobleme</font>aufzuteilen und so schrittweise zu lösen (Problemreduktion, vgl.[NIL71]), kombinierte <font COLOR="0000FF">Bledsoe</font> mit der Idee, schon bewieseneHilfssätze zur Beweisunterstützung heranzuziehen (Resolution-Theorembeweiser beweisen ständig primitive Tatsachen aufs neue) und den Menschen im <font COLOR="FF0000">Dialog</font> anzusprechen, falls einUnterziel nicht erreicht werden konnte. Dem gegenüber nimmt der Dialog bei Resolutionsbeweisern, mit denen allenfalls auf die Strategieauswahl Einfluß genommen werden kann [ALL69], einen prinzipiell bescheidenenPlatz ein. </p> <p>Verbessert wurde die Basis der Nicht-Resolutionsbeweiser durch die Übernahme der <font COLOR="0000FF">Gentzen</font>schen Regeln des natürlichenSchließens [GEN35] als grundlegende Schluß-regeln. Damit wurde dieStrukturangepaßtheit verbessert und vertieft. </p> <p>In seinem Überblick über die Methoden der ``natürliche'' Theorembeweiser erwähnt <font COLOR="0000FF">Bledsoe</font> folgende Grundkonzepte[BLE75b]:</p> <p>\begin {itemize} </p> <li>Benutzung von Datenbasen mit <font COLOR="FF0000"> relevantem Wissen</font>: Die Axiomeund beim Beweis erhaltene Fakten über Objekte, die im Beweis eine Rolle spielen, werden hier aufbewahrt und benutzt, wenn solche Fakten gefragt werden. </li> <li><font COLOR="FF0000">Reduktion</font> komplizierter Prädikate zu einfacheren: Umeinen Beweis auf möglichst abstrakter Ebene ablaufen zu lassen, werden die Theoreme mit komplexen Begriffen (Prädikaten) formuliert. Um die Verknüpfung dieser Begriffe für den Beweis auszunutzen, werden die Begriffsdefinitionen als Ersetzungsregeln für die Prädikate vom Nutzer angegeben. Wenn die Zerlegung eines komplexen Prädikats für den Beweis erforderlich wird, wird es entsprechend der Regel durch das Definiens ersetzt. In ähnlicher Form lassen sich auch Hilfssätze verwenden (bedingte Ersetzung). </li> <li>Algebraische <font COLOR="FF0000">Vereinfachung</font>. Häufig tauchen kleineTeilausdrücke auf, in denen ganze oder reelle Zahlen eine wichtige Rolle spielen. Wollte man nun die Axiome für diese Zahltheorien hinzufügen und beim Beweis als normale Fakten in der Datenbasis berücksichtigen, würde der Ablauf stark verlangsamt. Statt dessen bevorzugt man eingebaute Vereinfacher, die die üblichen Eigenschaften der Zahlen und ihrer Verknüpfungen ausnutzen (Kommutativität der Addition, der Multiplikation usw.) </li> <li>Spezielle Methoden für Ungleichungen: Auch Ungleichungen tretenhäufig auf. Angepaßte Programme sparen viel Zeit. </li> <li>Verwendung ``natürlicher'' Schlußregeln zur {\em Ausnutzungstruktureller Eigenschaften} des zu beweisenden Theorems. </li> <li>Ableitung zusätzlicher ``Voraussetzungen'' durchvorwärtsgerichtete Deduktion. </li> <li>Steuerung der Beweissuche durch ein koordinierendes Programm.</li> <li>Spezielle Hinweise (advice), daß unter gewissen Umständen bestimmte Hilfssätze verwendet werden sollten. </li> <li>Einbau von Experten-Systemen (Gruppen von problemspezifischenProzeduren) zur Lösung immer wiederkehrender Teilprobleme (z.B. für Induktion, Grenzwertbildung etc.). </li> <li>Benutzung von Modellen und Gegenbeispielen.</li> <li>Benutzung von Analogieschlüssen (ein ähnliches Theorem solltemit ähnlichen Mitteln beweisbar sein). </li> <li>Dialog.\end {itemize} <p>Es ist sicher, daß auch die ``natürlichen'' Systeme gegenwärtig noch nicht bei der Beweisfindung neuer Theoreme eingesetzt werden können. Man darf aber erwarten, daß Theorembeweiser vom Format des UT-interactive-theorem-prover [BLE75a] bemerkenswerte Beiträge auf demWege dorthin leisten werden (siehe aber [BROW78]).</p> <h2>Beweisüberprüfung</h2> <p>&nbsp;</p> <h3>Das Problem</h3> <p>Das gegenwärtige Wissen über Beweisverfahren und ihre mögliche Effizienz kann keinesfalls fortgeschritten genannt werden. Die junge Wissenschaftsdisziplin des Theorembeweisens kann zwar beeindruckende Ergebnisse vorweisen, für umfassende praktische Anwendungen reicht der derzeitige Stand jedoch nicht aus. Dies ist kein Wunder bei einer so komplexen Materie und sollte nicht entmutigen. </p> <p>Um Mathematikern und Logikern bei ihrer täglichen Arbeit zu helfen, sind deshalb Systeme entwickelt worden, die einen pragmatischen Zweck verfolgen: Statt den Beweisprozeß zu automatisieren, wird nur die <font COLOR="FF0000"> Verwaltungsarbeit</font> für Beweise automatisiert. Dabei versuchtman, den Verarbeiter für Beweiszeilen so zu erweitern, daß Korrektheitsprüfungen durchgeführt werden. </p> <p>Das Problem, Beweise in einem formalen System zu überprüfen, ist, verglichen mit dem Problem, diese Beweise zu finden, von einem geringeren Komplexitätsgrad. Die Resultate von {\sc Gödel, Tarski, Turing} und <font COLOR="0000FF"> Church</font> zeigen, daß allgemeine Beweisverfahren nurin sehr begrenzten formalen Systemen (etwa im Aussagenkalkül) konstruierbar sind; Beweise können aber in jedem formalen System überprüft werden. </p> <p>Ein Beweisüberprüfer (proofchecker) könnte recht einfach programmiert werden, wenn die benötige Eingabe (die in der passenden formalen Sprache geschriebenen Beweise) geliefert werden könnte. Da dies aber im allgemeinen jeden Benutzer überfordert, wenn man sich etwa mit der üblichen Prädikatenlogik 1. Stufe samt ihren Beweisregeln begnügt, muß das Program mehr leisten, als man im ersten Augenblick wahrhaben möchte. </p> <p>Zwei Probleme stehen dabei im Blickpunkt: Dem Nutzer soll eine relativ natürliche Eingabeform ermöglich werden, und er soll sich solcher Beweisschritte bedienen können, die in normalen Beweisen vorkommen. Das heißt also, man hat ein formales System aufzustellen, dessen Schlußregeln und dessen Ausdruckskraft (Formulierungsmittel) die mathematische Praxis weitgehend widerspiegelt. </p> <p>&nbsp;</p> <h3>Drei Beweisprüfer </h3> <p><font COLOR="0000FF">John McCarthy</font> hatte schon 1961 einen Beweisüberprüfer vorgeschlagen [MCC61a]. Auf seine Anregung hin schrieb <font COLOR="0000FF">P.Abrahams</font> eine Dissertation zu diesem Thema [AB63], die 1963 abgeschlossen vorlag.</p> <p><font COLOR="0000FF">Abrahams</font> Beweisüberprüfer bestand aus zwei Teilen: DemGenerator für den vollständig formalisierten Beweis (engl. rigorous proof) aus der Eingabe und dem eigentlichen Überprüfer. Beide Teile waren als Coroutinen gekoppelt. Immer wenn der Generator einen Beweisschritt erzeugt hatte, verarbeitete der Überprüfer diesen Schritt und akzeptierte ihn bzw. lehnte ihn ab. </p> <p>Die Eingabe der Beweisschritte erfolgte über eine Art Makrosprache, die der Nutzer nach einigem Gutdünken erweitern konnte. {\sc Abrahams} zieht in [AB64] eine enge Parallele zwischen Programmierenund Beweisen und argumentiert, daß die eigentlichen Schlußregeln des formalen Systems auf dem gleichen Niveau stünden wie bei der Programmierung die Maschinenbefehle. Um die kleinen Schritte zu kombinieren und zu beherrschbaren, verständlichen Einheiten zusammenzufassen, sei ein synthetischer Ansatz, wie er eben in der Makrosprache zum Ausdruck komme, äußerst passend. </p> <p>Unter den bereitgestellten Makros war z.B. der {\em Modus Ponens} -- eine Regel, durch die Abtrennungen an Implikationen durchgeführt und Substitutionen angegeben werden konnten, um diese logische Schlußweise anwenden zu können. Ein anderes Makro löste die $\lambda$-<font COLOR="FF0000">Konversion</font> [CH41] aus, ein weiteres den Versuch,eine bestimmte Konklusion aus einer gegebenen Prämisse abzuleiten. </p> <p>Aus diesen Makros wurden die Beweisschritte generiert, die die formalen Schlußregeln enthielten. Davon waren zehn vorhanden: Regeln für die Einführung von Axiomen und bewiesenen Sätzen, für die Ausführung rein aussagentheoretischer Ableitungsschritte (darunter auch der eigentliche Modus Ponens), einige für Berechnugen und zwei für die Verarbeitung von Quantoren (``für alle'', ``es gibt ein''). Schließlich gab es noch eine Regel für die Benutzung von Definitionen. </p> <p>Die Beweisschritte, die dem Überprüfer übergeben wurden, bestanden aus dem Namen der Schlußregel (besser: des Schlu\ss operators) und aus ihren Parametern: Wollte man etwa ein bereits bewiesenes Theorem benutzen, so hatte man den Operator USETHManzugeben, den Namen des Theorems und die Liste der Substitutionen für die Variablen. </p> <p>Der Überprüfer analysierte einen solchen Schritt und erzeugte aus ihm eine Beweiszeile, falls die Prüfung erfolgreich verlief. Eine solche Zeile bestand aus der Zeilennummer, dem Text der Zeile, d.h. der mit dem Beweisschritt bewiesenen Aussagen, und eine Liste von Voraussetzungen, von denen die Zeile abhing. </p> <p>Ein Beweis war vollendet, wenn der Text der letzten Zeile dem zu beweisenden Theorem entsprach und keine Voraussetzungen in der Zeile auftauchten. </p> <p>Leider ist die genaue Syntax der Eingabesprache nicht bekannt. Diese Sprache scheint aber der LISP S-Sprache sehr ähnlich gewesen sein, wenn man die Makrodefinition betrachtet ([AB64], S. 153):<plaintext> ((L1 L2) (L3) (SETQ L3 (FINDLINE L2)) (CONJOIN (LIST L1 L2)) (USETHM (QUOTE EQL1) (LIST (CADR L3) (CADDR L3))) (MODUS (LCM 2) (LCM 1))) </plaintext>Dies ist die Definition für ein sogennantes internes Makro zur Erzeugung von B, falls die zwei Aussagen A und {\tt(EQUAL A B)} existieren. </p> <p>1972 baute <font COLOR="0000FF">R.Milner</font> den Beweisüberprüfer für einenformalen Kalkül für berechenbare Funktionen ({\em Logic for Computable Funktions)} von <font COLOR="0000FF">D.Scott</font> [SCO69a] auf, das {\tx LCF}-System [MIL72a]. In diesem System werden die Beweise in der Formvon Kommandofolgen eingegeben. Es gibt Kommandos zum Einführen von Axiomen sowie Annahmen, zum Ausführen von Schlußregeln und zum Manipulieren des jeweiligen Ziels (des zu beweisenden Theorems). Neu bei {\tx LCF} ist, daß die Beweisschritte nicht nur verwaltet und überprüft werden, sondern das System führt einige Schritte auch von allein aus, ohne daß der Benutzer dies in einzelnen fordern muß. </p> <p>Um den Umgang mit dem Beweisüberprüfer zu erleichtern, ist dieser auf einem formalen System aufgebaut, dessen Schlußregeln dem Kalkül des <font COLOR="FF0000">natürlichen Schließens</font> [GEN35] entsprechen.Hinzugenommen wurden weitere, dem {\tx LCF}-Kalkül angemessene Regeln, die dem Benutzer als Kommandos verfügbar sind. </p> <p>Übliche Aufgabe, vor der der Benutzer steht, ist der Beweis einer Aussage über ein Programm unter Voraussetzung von Annahmen über die benutzte Programmiersprache. {\tx LCF} ist für die Dialogarbeit konzipiert: Zeilenweise werden die Kommandos eingegeben, das System überprüft sofort und baut intern eine Beweisstruktur auf. Dabei kann der Benutzer das Beweisziel in einzelne Teilziele aufspalten und neue Unterziele einführen, die seiner Meinung nach zum Erreichen eines solchen Teilziels nötig sind. Das System kennt die Hierarchie dieser Ziele und erleichtert dem Nutzer die Verwaltung. Es hilft sogar so weit, daß man etwa angeben kann, durch welches Beweiskommando ein gegebenes Ziel vermutlich erreicht wird und nun die für die Anwendung dieses Kommandos nötigen Voraussetzungen als neue Unterziele erzeugt werden. </p> <p>{\tx LCF} ist für Beweise von Programmen und Aussagen über rekursive Funktionen verwendet worden [MIL72b. c. WEY72, NEW74]. EineTeilmenge ohne den Unterzielmechanismus und mit einigen Ersatzkommandos wurde 1974 als {\tx LCF-small} von <font COLOR="0000FF">Aiello</font> und <font COLOR="0000FF"> Weyhrauch</font> implementiert [AW74].</p> <p>Für den Prädikatenkalkül 1. Ordnung haben <font COLOR="0000FF">Weyhrauch</font> und<font COLOR="0000FF">Thomas</font>...</p> <p>Während in dem frühen System von <font COLOR="0000FF"> Abrahams</font> lediglich dieSymbolmanipulationsfunktionen von LISP (s. Abschnitt 3.5) eingesetzt wurden, so ist in den beiden neueren Systemen auch die Implementationssprache LISP genutzt worden: Hatte <font COLOR="0000FF">Abrahams</font> nochüber die unnatürliche Notationsweise geklagt ([AB64], S.159), sobieten sowohl {\tx LCF} als auch {\tx FOL} dem Nutzer gewöhliche mathematische Notationsweisen an. </p> <p><font COLOR="0000FF">Abrahams</font> belegte die Eignung von LISP für die Zwecke derBeweisüberprüfung mit Hinweisen auf die Möglichkeiten zum Backtracking (vgl. 3.9.3). Damit war es möglich, Verarbeitungsschritte auszulösen, die zu Systemfehlern führen, eine Fehleranalyse durchzuführen und die Resultate für die Fortführung des Programms zu verwenden. </p> <p>In {\tx FOL} beginnt der Nutzer damit, daß er dem System die verwendete <font COLOR="FF0000">Zeichenkonvention</font> mitteilt und wichtige {\emGrundbegriffe} vereinbart. Anschließend wird er gewöhnlich die verwendeten <font COLOR="FF0000">Axiome</font> eingeben. Mit diesen Schritten wird also,kurz gesagt, der theoretische Rahmen festgelegt. Hinter der Einführung des Zeichen- bzw. Namensgebrauchs steht die Fähigkeit, mit verschiedenen Sorten von Objekten umgehen zu können: Ist in nahezu jeder mathematischen Theorie das Wissen über die Arbeit mit natürlichen Zahlen erforderlich, so kommt meistens hinzu, daß der Mathematiker es gleichzeitig mit verschiedenartigen Objekten zu tun hat, z.B. Mengen, Klassen, Funktionen von Mengen in Mengen usw., und daß er diese Objekte schon an ihren Namen unterscheiden möchte. Dies ermöglicht {\tx FOL} durch die <font COLOR="FF0000">Sorten</font>. </p> <p>Da die Basis vieler theoriespezifischer Beweistätigkeit oft die <font COLOR="FF0000">Mengelehre</font> ist, bietet {\tx FOL} vorfabrizierte Sequenzen vonDeklarationen für Sorten und Definitionen von Axiomen für bekannte Systeme der Mengelehre an. Daneben kann man auch modale Kalküle abrufen. </p> <p>Die eigentlichen Arbeitskommandos sind Einführungs- und Beseitigungsregeln für die verschiedensten logischen Junktoren. Diese entsprechen ihren Vorbildern in <font COLOR="0000FF"> Prawitz</font>' natürlichemDeduktionssystem [PRAW65]. Daneben sind Regeln zur Feststellung vonTautologien, Entscheidungsprozeduren für die Theorie der Gleichheit sowie explizite Substitutionsregeln und Unify-Kommandos (Vergleich von Formeln, die ähnliche aussagenlogische Formen haben, durch Manipulation der Quantoren und passende Substitutionen) verfügbar. Auch Vereinfachungen von funktionalen Ausdrücken durch Herstellung von Beziehungen zu LISP-Funktionen können durchgeführt werden. Wichtigster Anwendungsfall sind natürlich arithmetische Ausdrücke. </p> <p>Die reinen Verwaltungskommandos sind so entworfen, daß sie dem Nutzer die Arbeit erleichtern: Einführung von Namen für Beweiszeilen, Arbeit mit Files, in die entweder eine Kopie der gegebenen Kommandos gerettet wird oder die als abzuarbeitende Kommandofolgen betrachtet werden usw. usf. </p> <p>Es dürfte interessant sein, Kommentare von Mathematikern zu hören, die sich dieses Systems bedient haben. Wann allerdings wirklich neue, komplizierte Sätze mit Hilfe eines ähnlichen Systems bewiesen werden können, bleibt abzuwarten. </p> <p>&nbsp;</p> <h2>Programmverifikation</h2> <p>&nbsp;</p> <h3>Das Problem</h3> <p>Es ist eine bekannte und beklagenswerte Tatsache, daß Programme meist Fehler enthalten, d.h., sie liefern nicht immer das Ergebnis, das man von ihnen erwartet. Je größer ein Programm ist, desto schwerer wird die Aufgabe, sich seiner Richtigkeit zu versichern. Die übliche Methode des Testens kann nur dann als ausreichende Prüfung bezeichnet werden, wenn die Struktur des Programms berücksichtigt wird [HU75];da es neben der vom Programmierer explizit angegebenen Struktur des Programmablaufs auch eine implizite gibt,\footnote { Die meisten modernen Rechner interpretieren die vom Nutzer in der einen oder anderen Urform gelieferten, schließlich als Folge von sogennanten Maschinenbefehlen vorliegenden Programme durch Mikroprogramme unsichtbar, die für den Programmierer sonst uninteressant sind -- im Fehlerfall werden über sie Unterbrechungen ausgelöst, z.B. bei Zahlenüberläufen oder Division durch Null.} erfordert ein vollständiger Test eigentlich ein vollständiges Abarbeiten aller möglichen Eingabewerte. </p> <p>Durch die kombinatorische Explosion ist ein umfassender Test praktisch undurchführbar -- Testen beschränkt sich daher auf die Auswahl möglichst typischer bzw. kritischer Beispiele. Hier hat auch die Feststellung ``Testen kann nur die Existenz eines Fehlers zeigen, aber niemals seine Abwesenheit'' [DA72] ihren Ursprung. Man beachteübrigens, daß Tests nicht nur durchgeführt werden, um die Richtigkeit eines Programms festzustellen, sondern auch, um das Programmverhalten überhaupt zu erkunden. </p> <p>Gegenüber dem Ausprobieren einzelner Anwendungsfälle hätte der Beweis, daß ein Programm seinen Spezifikationen genügt, den Vorzug, daß mit ihm für <font COLOR="FF0000">alle</font> Eingabedaten die Korrektheitfeststünde. Allerdings wird dieser Gewinn mit anderen Komplikationen bezahlt: Der Programmierer muß die Spezifikationen für sein Programm in einer formalen Sprache angeben. Meist wird hierfür der Prädikatenkalkül erster Stufe verwendet. So kann diese Aufgabe {\em genauso schwierig} sein wie das Programmieren selbst. </p> <p>Für größere Programme können solche Beweise nicht geführt werden, da die Menge der anfallenden Arbeiten menschliche Möglichkeiten übersteigt. Demnach benötigt man automatische Beweiser für diesen Zweck. Diese Beweiser wiederum haben derzeit noch nicht die Leistungsfähigkeit, die man im allgemeinen Fall brauchen wird. </p> <p>Beide Probleme sind für die Programmverifikation eigentlich nur Randprobleme; dennoch verliert sie ihren Sinn, wenn diese nicht akzeptabel gelöst sind. Die bisherigen Systeme für die Verifikation von Programmen [GOO75b,SUZ76,HOO76,SCHO78] versuchen das erste Problemdadurch zu bewältigen, daß der Prädikatenkalkül durch Definitionsmöglichkeiten angereichert wird. Indem der Nutzer Definitionshierarchien für seine Prädikate (die problemspezifischen Begriffen entsprechen) und Hilfssätze über ihre Zusammenhänge angibt, wird es ihm möglich, die Programmspezifikationen problemnah und weitgehend natürlich niederzuschreiben. </p> <p>Das zweite Problem bleibt ein Problem für den Wissenschaftszweig des Theorembeweisens (siehe Abschnitt 2.3). Um die Programmverifikatoren praktisch anwendbar zu machen, hat man nicht nur existierende Theorembeweiser [GOO75b,IG73], sondern auch ganz angepaßte Programmeeingesetzt [SUZ76,HOO76]).</p> <p>Wenn bisher keine wirklich großen Programme automatisch bewiesen wurden, so kann man dennoch sagen, daß die Programmgröße an sich nicht die Hauptschwierigkeit ist. Wenn es möglich ist, die Spezifikationen anzugeben, sollte auch ein Beweis möglich sein. Allerdings stellt für ein einigermaßen kompliziertes Programm von der Größenklasse eines Compilers oder Betriebssystems die Aufgabe, die Eingabe- und Ausgabebedingungen anzugeben, ein großes Problem dar (obwohl schon Teile von Compilern bewiesen wurden [LON71,PAI67]).</p> <p>&nbsp;</p> <h3>Ein typisches Programmverifikationssystem</h3> <p>Üblicherweise besteht ein Programmverifikationssystem aus drei Hauptteilen: Einem Programmteil für die Umsetzung der Quellprogramme samt den Programmspezifikationen in eine interne Form, einem Programmteil für die Erzeugung logischer Theoreme aus diesen Eingabedaten (Erzeugung der sogenannten Verifikationsbedingungen) und schließlich dem Theorembeweiserprogramm. </p> <p>Hier wollen wir uns nur mit dem Theoremerzeuger befassen, da über Theorembeweiser im Abschnitt 2.3 und über Sprachimplementation im Abschnitt 2.7 einiges zu finden ist. Man beachte dabei in beiden Fällen, daß es einige spezifische Aspekte für die Anwendung derartiger Programme für die Zwecke der Programmverifikation gibt, daß aber diese Besonderheiten bei einer Einführung in die Probleme nicht ins Gewicht fallen. </p> <p>Die Generierung der Verifikationsbedingungen erfolgt üblicherweise nach dem Verfahren der <font COLOR="FF0000"> induktiven Assertions</font> [IG73, FL67a].Dieses Verfahren verlangt, daß jeder mögliche Weg durch das Programm mit einer Anfangsbedingungen beginnt und nach der letzten Programmanweisung eine Endebedingung besitzt. Als verschiedene Wege durch das Programm werden Folgen von Anweisungen verstanden, die von einem (dem) Anfangspunkt nach einem (dem) Endpunkt führen und sich mindestens in einer Anweisung unterscheiden. Wenn in Programm also eine Weiche ({\tt if}... then... else) auftritt, dann verläuft eineGruppe von Wegen durch den then-Teil und eine andere durch denelse-Teil. Je mehr solche Weichen vorhanden sind, desto mehrunterschiedliche Wege gibt es im Programm. </p> <p>Zu den Wegen, die vom Programmanfang zum Programmende führen (viele, wenn nicht die meisten Programme besitzen jeweils nur einen solchen Punkt) kommen noch die geschlossenen Wege im Programm, die Zyklen, hinzu. Auch für diese Wege wird gefordert, daß am Anfang und am Ende jeweils eine Bedingung stehen muß. Die Besonderheit der Zyklen besteht darin, daß beide Bedingungen zusammenfallen. Diese Zyklenbedingungen enthalten daher im Allgemeinen Aussagen über Zyklenkonstanten (etwa über gleichbleibende Konvergenzrichtungen o.ä., siehe [BAS75]) und werden für die induktiven Zyklenbeweisebenötigt (daher ``induktive Assertions''). Es leuchtet nun unmittelbar ein, daß ein Programm besonders gut analysierbar ist, wenn die Wege ohne Sprungbefehle (goto) programmiert sind: Die Suche nach derFortsetzung des Weges kann im Einzelfall sehr kompliziert sein, wenn das Programm nicht wohlstrukturiert ist [DA72] bzw. wenn nicht höhereSprachelemente für die Formulierung von Zyklen und Programmweichen verwendet worden sind. </p> <p>Da ein Programm nur zusammen mit den geforderten Anfangs- bzw. Endbehauptungen (<font COLOR="FF0000">Assertions</font>) verarbeitet werden kann, muß jemand, im allgemeinen der Programierer, diese in den Programmtext aufgenommen haben. Es war schon darauf hingewiesen worden, daß hier ein erhebliches Problem liegt, insbesondere, wenn die Assertions einem fertigen Programm hinzugefügt werden sollen. Um hier zu einer Erleichterung zu kommen, wurde vorgeschlagen, auch die Assertions während der Programmentwicklung nach und nach aufzubauen \cite{GOO75a, WU76}. Es gibt auch Versuche, Zyklenassertions im Nachhinein aus dem Programmtext zu generieren [GER75].</p> <p>Beinahe alle Programmverifikationssysteme sind in LISP bzw. in auf LISP aufbauenden Sprachen geschrieben worden. Das liegt daran, daß ein Programm sehr leicht in eine Listenstruktur übergeführt, und daß diese dann sehr bequem durch den Generator für die Verifikationsbedingungen verarbeitet werden kann. </p> <p>Dieser Generator ist ein rekursives Programm, weil die Wege durch das Programm aus Programmanweisungen bestehen, die selbst wieder Programmanweisungen enthalten können (Blockverschachtelung, Möglichkeiten, in Zyklenkonstruktionen Anweisungen zu schreiben, usw.). Während das Verifikationssystem von <font COLOR="0000FF">King</font> [KIN69], daserste arbeitsfähige System, die unterschiedlichen Wege noch generierte und einzeln durcharbeitete, kann ein rekursiv arbeitender Generator Wegverzweigungen durch rekursiven Aufruf für die einzelnen Zweige behandeln. </p> <p>Die Bearbeitung des Programms kann prinzipiell in zwei Richtungen erfolgen, vorwärts oder rückwärts [GOO70], jedoch hat sich dierückwärtige durchgesetzt. Das Programm wird also vom Ende anfangend durchgearbeitet, dabei werden entsprechend der jeweils letzten Programmanweisung Aktionen durchgeführt, indem entweder der Generator rekursiv wieder aufgerufen wird (etwa für Zyklenanweisungen) oder die Endebedingungen manipuliert wird. </p> <p>Die für jede Anweisungen erforderlichen Aktionen werden aus Schlußregeln einer durch <font COLOR="0000FF">Hoare</font> [HOA69] eingeführtenProgrammlogik abgeleitet [IG73]. Besonders durchsichtig ist hier dieRegel für die Zuweisung. Um diese angeben zu können, müssen wir einige Notationsweisen von <font COLOR="0000FF">Hoare</font> einführen.</p> <p>Wenn eine bestimmte Bedingung Q gilt, falls einProgrammstück A abgearbeitet wurde und vorher die BedingungP gegolten hat, so schreiben wir<plaintext> P{A}Q </plaintext>Programmteile bestehen aus Anweisungen, die durch Semikolon voneinander getrennt sind. Wir notieren dabei meist nur die interessierenden Anweisungen und fassen die übrigen in einem Programmstück zusammen: <plaintext>A;x:=1 A';while y<n do x:="x*a;" </PLAINTEXT />Wenn wir zu einem Programmteil Anweisungen hinzufügen können, ohne daß sich die Endebedingung ändert (bzw. daß die alte falsch wird), wollen wir dies so notieren, daß die alte Programmaussage über einen Strich geschrieben wird und die neue unter einen Strich: </p> <p>\vspace{0.5mm} </p> <p>\begin{center}{\LARGE $\frac{(X=3)\{A\}(X=Y+3)}{(X=3)\{A;z:=1\}(X=Y+3)}$.} \end{center} </p> <p>\vspace{0.5mm} </p> <p>Einen derartigen Ausdruck nennen wir ``Schlußregel''. Wenn die zum Programm A hinzugefügte Anweisung für die Endebedingungrelevant ist, dann wird unter dem Strich eine andere Endebedingung stehen als oben. </p> <p>Damit sind genug Notationsmittel eingeführt, um die Regel für die einfache Zuweisung angeben zu können: </p> <p>\vspace{0.5mm} </p> <p>\begin{center}{\LARGE $\frac{P\{A\}Q(e)}{P\{A;x:=e\}Q(x)}$.} \end{center} </p> <p>\vspace{0.5mm} </p> <p>Hier bedeutet Q(x) den logischen Ausdruck, der aus Q(e)durch Substitution von x und e hervorgeht (möglicheNotation: Q(x/e)).</p> <p>Da die Mehrheit der eigentlichen Programmaktionen in Zuweisungen besteht und bei der Verarbeitung jeder Zuweisung der angegebenen Regel folgend eine Substitution durchzuführen ist, heißt die Methode, nach der die Programme rückwärts entsprechend den Schlußregeln durchgearbeitet werden, <font COLOR="FF0000">backward substitution</font>. Allerdings werden nundiese Regeln zur Zerlegung und nicht zur Komposition des Programms benutzt und von unten nach oben gelesen: Wenn das Programm A;x:=eunter der Anfangsbedingung P der Endebedingung Qgenügen soll, dann muß das Programm A unter derAnfangsbedingung P der Endebedingung Q(e/x) genügen(der Teilausdruck e/x bedeutet keine Division, sondern zeigt dieSubstitution an). </p> <p>Der Generator für die Verifikationsbedingungen hat, entsprechend dieser Notationsweise, drei Argumente: Die Anfangsbedingung, das Programm und die Endebedingung. Alle drei liegen als Listenstruktur vor, und sowohl die Durcharbeitung als auch die Substitution lassen sich leicht in LISP programmieren. Wenn etwa die dem Programm entsprechende interne Listenstruktur so gewählt ist, daß der Typ der letzten Anweisung (bzw. des ersten Listenelements, falls die Liste das umgekehrte Programm repräsentiert) aus dem ersten Element der Teilliste ermittelt werden kann, die die Anweisung darstellt, dann läßt sich das Generatorprogramm ziemlich direkt aus den Schlußregeln ableiten ([IG73], S. 34).</p> <p>Die logischen Theoreme entstehen immer dann, wenn ein Weg bis zu Ende abgearbeitet wurde: Konkret dann, wenn Zyklenkonstruktionen auftauchen (die in ihrer Gesamtheit einen Weg repräsentieren) oder wenn das Programmstück leer geworden ist. Da für ein leeres Programm eine Anfangsbedingung die Endebedingung implizieren muß, damit diese gilt, werden durch den Generator Implikationen erzeugt, die für einfache Wege aus der Anfangsbedingung (Prämisse) und der veränderten Endebedingung (Hypothesis) bestehen, während für Zyklen die Anfangsbedingung aus dem induktiven Assertion und der Zyklusbedingung (die Bedingung, entsprechend der der Zyklus weiter durchlaufen wird) und die Endebedingung aus dem veränderten Zyklus-Assertion besteht. </p> <p>Wenn für eine Programmiersprache einmal ein System von Schlußregeln formuliert ist, liegen die Probleme bei der Erstellung des Verifikationsbedingungsgenerators bei der Behandlung von allgemeinen Datenstrukturen. Kleinere Komplikationen bringen verschachtelte {\tt IF}-Anweisungen und Prozeduraufrufe mit sich. In der Literatur werden diese Fälle ausreichend besprochen [IG73].</p> <p>Die erzeugten Theoreme werden dann an den Theorembeweiser weitergereicht. Oft reicht schon eine arithmetische Vereinfachung aus, um den Beweis trivial werden zu lassen. Sollte ein Beweis einmal versagen, weil das Teiltheorem falsch ist, so kann man eine Beziehung dem Theorem und dem Programmstück herstellen, in dem der Fehler liegen muß. Allerdings können auch die Assertions (Spezifikationen) falsch sein. Durch einen iterativen Berichtigungsprozeß können schließlich auch diese Programmteile verifiziert werden [HEN75].</p> <p>&nbsp;</p> <p>&nbsp;</p> <h2>Formelmanipulation</h2> <p>&nbsp;</p> <h3>Das Problem</h3> <p>Jeder Praktiker, der viel mit mathematischen Formeln zu tun hat, kann ein Lied davon singen, wie zeitaufwendig die Arbeit mit ihnen sein kann. Nach tagelanger mühevoller Beschäftigung mit seitenlangen Formelschlangen, Differentiationsaufgaben, Lösung komplizierter Integrale und Ausmultiplizier- bzw. Ausklammerungsaufgaben kann eine elegante Lösung gefunden sein, deren Richtigkeit offensichtlich sein mag; aber oft auch dürfte es vorkommen, daß die Überprüfung wieder Tage dauert. Viele der wissenschaftlichen Fragestellungen werden schließlich durch numerische Auswertung der Formeln beantwortet, die das Problem beschreiben. Die analytische Vorbereitung dieser Rechnungen kann mit erheblichem Effekt verbunden sein: Manchmal erreicht man sogar, daß die Lösung überhaupt symbolisch angegeben werden kann -- eine Integration kann nach Regel der bestimmten Integration durchgeführt und durch Einsetzen von Grenzen eine <font COLOR="FF0000">exakte</font> Zahl ermitteltwerden. Oder eine gesuchte Formel muß nicht durch Approximation gesucht werden, sondern man kann sie als symbolischen Ausdruck hinschreiben. In vielen ähnlichen Fällen hat die analytische Aufbereitung den Vorteil, daß ein <font COLOR="FF0000">exaktes Ergebnis</font> erreichtwird, während ein numerisches Verfahren von vornherein mit der Problem der <font COLOR="FF0000">Rundungsfehler</font> und der <font COLOR="FF0000">Fehlerfortpflanzung</font> belastetist. </p> <p>Gar nicht so selten sind Situationen gegeben, wo numerische Verfahren überhaupt versagen. Es kann sein, daß entweder die Verfahren selbst sehr empfindlich sind oder die Problemsituation so ungünstig ist, daß sich zwar Ergebnisse berechnen lassen, die aber praktisch unbrauchbar sind: Die Fehler sind vielleicht betragsmäßig größer als das Ergebnis selbst. </p> <p>In einem solchen Fall kann eine symbolische Lösung die {\em einzig mögliche} sein. Oft haben einige analytische Vorbehandlungen des Problems den Effekt, daß zu einem günstigeren Ausgangspunkt vorgestoßen werden kann. </p> <p>So kann in einzelnen Fällen die symbolische Rechnung wesentlich <font COLOR="FF0000">billiger</font> und <font COLOR="FF0000">effektiver</font> sein als die numerische. Meistaber wird durch <font COLOR="FF0000">günstige Kombination</font> beider Verfahren eineenorme Kosteneinsparung erreicht werden. </p> <p>Ein Program, das dem Wissenschaftler diese mühevolle und größtenteils mechanische Arbeit abnehmen könnte, wäre ein Segen für die wissenschaftliche Welt, möchte man meinen. Nun existieren Formelmanipulatiosysteme für die praktische Anwendungen seit Beginn der sechziger Jahre (z.B. [HEA64,HEA67,HEA73]). Überraschenderweise ist die Nutzerzahl aber nicht so groß, wie man erwartet könnte. Wie <font COLOR="0000FF">Cohen</font> et al. [CO76] schreiben, habe man den Eindruck, daß esmehr Systeme für die Formelmanipulation gebe als Nutzer (vgl. dagegen <font COLOR="0000FF">Fitch</font>s Feststellung vom ``schleichenden Durchbruch'' [FIT79]).</p> <p>Ursache dieser Situation ist nicht nur die Tatsache, daß die Existenz dieser Systeme nur einem kleinen Kreis von Eingeweihten bekannt ist. Denn wären die Erfolge der benutzenden Wissenschaftler aufsehenerregender als die der übrigen, dann würde der Nutzerkreis schnell anwachsen. Nur in Wissenschaftsbereichen, in denen man derartig große Formelmengen bewältigen muß, daß ein Verzicht auf automatische Verarbeitung gleichbedeutend ist mit der Unmöglichkeit, überhaupt noch neue Forschungsresultate zu erzielen, haben sich die Formelmanipulationssysteme weitgehend durchgesetzt. Ein Beispiel hierfür ist die Relativitätsphysik [CO76].</p> <p>Für den potentiellen Nutzer eines solchen Systems besteht zunächst das <font COLOR="FF0000">Zugriffssproblem</font>: Wenn er nur schwer an einenRechner herankommt und Stunden damit verbringen soll, eine konkrete Formelmanipulationsaufgabe vozubereiten (die Mühe überhaupt Rechenzeit zu bekommen; der Kampf mit dem Rechenzentrum, und dessen nutzerfeindliche Festlegungen aufzuweichen bzw. überhaupt vollständig zu erfahren; die Frage, ob Direktzugriff möglich ist, oder ob zunächst Datenträger vorzubereiten sind: Lochkarten implizieren Lochfehler usw. usw.), dann wird er doch lieber mit seiner erprobten sicheren Bleistift-Papier-Methode vor ankommen. Kurz gesagt: Formelmanipulation lohnt sich erst, wenn man im Dialog arbeiten kann\footnote{ Früher konnten Formelmanipulationssysteme nur auf den großen Zentralrechnern laufen. Seit die Personalcomputer mehr Kapazität haben als die zentralen Rechnern hat sich die Situation fundamental gewandelt.}. </p> <p>Es gibt aber eine Reihe von Problemen, die die Formelmanipulationssysteme direkt angehen: Da ist zunächst das Problem der <font COLOR="FF0000">Eingabe der Daten</font>. Ein restriktivesFormelmanipulationssystem, das vom Nutzer ein ihm völlig fremdes, unerklärliches Formelformat verlangt, weil dieses Format leichter verarbeitet werden kann, wird sicher weniger Nutzer finden, als ein System, das an üblichen Notationsweisen anknüpft. Wie sollen z.B. auf Lochkarten Summationsformeln untergebracht werden, die zweidimensional sind? Noch heute wird mit meist eindimensionalen Eingaben gearbeitet. </p> <p>Ein weiteres Problem bezieht sich auf die Verarbeitungsmöglichkeiten der Systeme: Zwar kann sich jeder Wissenschaftler noch einigermaßen vorstellen, daß etwa die symbolische Differentiation mechanisch durchführbar ist; aber die Zusammenfassung und die Vereinfachung? Es ist außerordentlich problematisch, was Vereinfachung überhaupt bedeutet: In einem {\em bestimmten Zusammenhang} kann die Formel (a+b)**2 einfacher seinals a**2 + 2*a*b + b**2, in einem anderen Zusammenhang abersicher die zweite Formel. </p> <p>Wie weit wird ein System integrieren können? Was darf man überhaupt an Möglichkeiten zur Strukturerkennung erwarten? Schließlich kann ein gegenwärtiger Rechner nur lineare Strukturen verarbeiten. Um zu einem mittleren Datenelement zu kommen, benötigt er eine Adresse oder bewegt sich Schritt für Schritt dorthin. Das Erfassen einer Struktur muß so äußerst langsam vor sich gehen im Vergleich zum schnellen Erfassen gerade struktureller Zusammenhänge durch den Menschen. </p> <p>Die Fähigkeiten, die ein derartiges System hat, und die Bequemlichkeit, mit der man sie ausnutzen kann, bestimmen demnach die Benutzerzahl in hohem Maße. </p> <p>Genauso wie die Eingabe bestimmt auch die Ausgabe die Handlichkeit eines Formelmanipulationssystems. </p> <p>Die Tatsache, daß die meisten wirklich benutzten Formelmanipulationssysteme von Fachleuten des Anwendungsgebietes entworfen und aufgebaut wurden, für das sie gedacht waren, zeigt, daß die Angepaßtheit und Nutzerfreundlichkeit vor der Effizienz den Nutzer anzieht. </p> <p>&nbsp;</p> <h3>Ein Beispiel für ein Formelmanipulationssystem</h3> <p>LISP wurde von Anfang an für Probleme der Formelmanipulation benutzt. Eine ganze Reihe von Systemen sind entweder in LISP programmiert worden bzw. sind in LISP-Systeme eingebettet [CO76,PRO66,PEK71]. </p> <p>Eines der am weitesten fortgeschrittenen Systeme ist {\tx MACSYMA} [BOG75]. Dies ist ein umfangreiches System für die Formelmanipulation,das am MIT Cambridge auf Grund der Erfahrungen mit einem allgemeinen Formelmanipulationssytem (MATHLAB [ENG65]), einem speziellerenSystem für die Integration (SIN [MOS67]) und einem weiterenFormelmanipulationssystem [MART67], das sich durch seine hervorragendenEin- und Ausgabemöglichkeiten auszeichnete, seit 1969 durch {\sc J.Moses, W.Martin} und <font COLOR="0000FF">C.Engelman</font> entwickelt wurde (heuteMATHLAB-Gruppe unter der Leitung von <font COLOR="0000FF">J.Moses</font>). {\tx MACSYMA}ist für den Dialogbetrieb gedacht: Der Anwender sitzt an einem Sichtgerät oder einer Workstation und gibt seine Formel bzw. Anweisungen über eine Tastatur ein. Die Eingabezeilen erscheinen auf dem Bildschirm und werden sequenziell durchnumeriert. Mit dem jeweiligen Endezeichen teilt man dem System mit, ob man das Resultat der Anweisung sehen will oder nicht. Während die Eingabe als eindimensionale Zeichenkette aufgebaut ist, gibt das System seine Antworten in einem zweidimensionalen Format aus. Ein Polynom mit Gliedern höherer Ordnung z.B. wird ausgegeben als: 4 2 8 Y - 8 Y + 1 [BOG75][S.13]Die entsprechende Eingabezeile würde lauten: 8* Y^4 - 8* Y^2 + 1; Rationale Ausdrücke werden in drei Zeilen ausgegeben, wenn Bruchstriche vorkommen: 2 SQRT (B - 4 C) + B X= - ------------------ 2 folgt als Antwort auf: SOLVE(X^2 + B*X + C,X); [BOG75][S.3]</p> <p>Zweidimensionale mathematische Symbole (Summationszeichen, Produktzeichen, Integrationszeichen) werden durch Hilfszeichen zusammengesetzt: Nach Eingabe von INTEGRATE (F(X),X,A,B)+X; erscheint B / I I F(X)DX + X. I / A [BOG75][S.54]</p> <p>Auch solche Ausdrücke wie die zur Maximum-, Minimum- und Grenzwertbildung werden in der üblichen zweidimensionalen Art angegeben: Nach Eingabe von LIMIT (F(R)^G(X + 1), X, 0, MINUS); erscheint LIMT F(X) G(X + 1). X 0- Die Eingabesprache ist eine ALGOL-ähnliche Ausdrucksprache (d.h. alle Sprachkonstrukte wie Zuweisung, Zyklenanweisung u.ä. haben einen Wert). Die Zahlen in dieser Sprache können beliebig groß bzw. beliebig genau sein; um effizient arbeiten zu können, sind sie in mehrere Typen eingeteilt. Auch die Namen, die im wesentlichen entsprechend den üblichen Regeln aufgebaut sein müssen, dürfen beliebig lang sein. Bei der Benutzung der Namen für Variable gibt es eine kleine Besonderheit: Hat die Variable noch keinen Wert bekommen (dies gilt auch für indizierte Variable), so wird als ihr Wert sie selbst genommen (also der Name; dies entspricht der Quotierung in LISP)! </p> <p>Zuweisungen werden auf die übliche Weise notiert, der Zuweisungsoperator ist ``:''. Die Operatoren in den Ausdrücken entsprechenden in Programmiersprachen üblichen (+,-,*,/,**), mit zusätzlichen kann der Nutzer die Auswertungsrichtung beeinflussen. Es gibt Möglichkeiten für die Definition von Funktionen, Feldern, Listen und Matrizen. </p> <p>Unter den Ausdrücken spielen die Gleichungen eine besondere Rolle. Da jede Eingabezeile und jede Ausgabezeile eine besondere Identifizierung tragen, kann man sich auf frühere Zeilen beziehen. Auf diese Art kann man etwa zwei Gleichungen addieren bzw. eine eimal angegebene Gleichung modifizieren: </p> <p>(C1) X+1 = Y^2 $ (C2) X-1 = 2*Y+1$ (C3) D1+D2; (D3) 2X = Y^{2}+2Y+1 </p> <p>Hier entsprechen die Zeilen D1 und D2 den Zeilen {\ttC1} und C2, sie sind wegen des \$-Zeichensunterdrückt worden. C bedeutet immer Eingabe, das Dimmer Ausgabe. </p> <p>Kompliziertere Berechnungen und Funktionen können mit Hilfe weiterer Sprachelemente ausgedrückt werden: Es gibt das IF-Statement,das Compound-Statement, Block-Konstruktionen und Zykluselemente (etwa in der Form des FOR-Statements in ALGOL). Alle diese Sprachelementescheinen für die normalen Zwecke ausreichen, die ein Nutzer verfolgen will; für besondere Wünsche gibt es Möglichkeiten, die Syntax zu ändern (durch Veränderung der Operatorenmenge und ihrer Eigenschaften). </p> <p>Ein zentraler Teil des Verarbeitungssystems ist, wie in den meisten ähnlichen Systemen, der <font COLOR="FF0000"> Vereinfacher</font>. Wir hatten schon ausgeführt,daß die Frage, ob ein gegebener Ausdruck einfacher sei als ein anderer äquivalenter im allgemeinen nur im Zusammenhang mit dem Zweck entscheidbar ist, den man mit dem vereinfachten Ausdruck verfolgt (es gibt natürlich eine genügend relevante Klasse von Vereinfachungsfällen, wo die Frage ganz klar beantwortet werden kann). Außerdem hat sich gezeigt, daß man für die verschiedenen Operatoren verschiedene Ausdrucksrepräsentationen verwenden sollte, um die Verarbeitung angepaßt und effizient ablaufen lassen zu können (vgl. zu den verschiedenen Formelmanipulatoren und den von ihnen benutzten Ausdrucksrepräsentationen [MOS71]). Man solltebesser von Transformationen zwischen wertgleichen äquivalenten Ausdrücken sprechen [MA75].</p> <p>Allerdings kann man die Frage, ob zwei Ausdrücke äquivelent sind, im allgemeinen Fall nicht entscheiden [RIC68]. Für praktisch wichtigeSpezialfälle (Polynome und rationale Funktionen) ist dies aber möglich, und es läßt sich eine kanonische Form angeben: Die Ausdrücke lassen sich so in einer bestimmten Weise standardisieren, daß Wertgleichheit mit Ausdrucksgleichheit zusammenfällt. </p> <p>MACSYMA versucht, für jeden Ausdruck eine kanonische Formzu finden (<font COLOR="FF0000">general form</font>); sind jedoch Elemente vorhanden, diedies unmöglich machen, dann wird ein Kompromiß versucht. Ganz grob gesprochen: Der Vereinfacher reduziert die Ausdrücke, indem er sie auf der Basis der vorher in sich geordneten Teilausdrücke ordnet. Konstanten stehen vor Variablen, diese vor Funktionsausdrücken. Die letzteren werden zunächst nach der Kompliziertheit der Argumente geordnet und nach ihren Namen, wenn die Argumente gleich sind [BOG75][S.28].</p> <p>Der Ausdruck X + 1 in der externen Form wird zu ((MPLUS SIMP) 1 \$X)vereinfacht. Die Unterliste, die hier als erstes Element auftritt, beschreibt den Ausdruck (er ist in diesem Fall schon vereinfacht, wie das Element SIMP andeutet), mit dem X und \$ wirdein Unterschied hergestellt zwischen Variblennamen des Nutzers und des Systems. </p> <p>Bei der Vereinfachung nutzt das Programm eine Menge von ``eingebautem Wissen'' über Algebra aus, versucht Brüche zu vereinfachen und Ausdrücke mit trigonometrischen Funktionen zu beseitigen. Dabei läßt sich manchmal keine strenge Trennung vornehmen zwischen der Auswertung eines Ausdrucks und seiner Vereinfachung. </p> <p>Eine Besonderheit des Vereinfachers in {\tx MACSYMA} ist die Möglichkeit, Teilausdrücke für sich allein behandeln zu können. Mit Hilfe von <font COLOR="FF0000"> Mustervergleichsmechanismen</font> (engl. pattern matching)werden viele Schritte der Vereinfachung ausgelöst. In {\tx MACSYMA} kann der Benutzer neue Transformationsregeln angeben oder alte entsprechend seinen Wünschen ändern. </p> <p>Die für Polynome und rationale Funktionen vorhandenen Verarbeitungsalgorithmen schließen neben <font COLOR="0000FF"> Horner</font>scherRepräsentationen, der Addition, Subtraktion, Multiplikation und Division vor allem die Bildung des größten gemeinschaftlichen Teilers und die Faktorisierung ein. Dabei wurden teilweise neueste Forschungsresultate dienstbar gemacht. Daneben existieren Teile für die Lösung linearer Gleichungssyteme und Systemen von Polynomgleichungen. </p> <p>Der Benutzer kann <font COLOR="0000FF">Taylor</font>-Entwicklungen veranlassen, Limites,Summen und Produkte auswerten, <font COLOR="0000FF">Laplace</font>-Transformationendurchführen und vieles andere mehr. Auch Tensor- und Matrixmanipulationen sind verfügbar. </p> <p>Ein wichtiger Teil des Systems ist im Integrationssubsystem zusammengefaßt. Es bestehet aus fünf Komponenten: Integration von rationalen Funktionen, dem Integrationsprogramm {\tx SIN} für Nicht-Standardintegrale, dem <font COLOR="0000FF">Risch</font>schen Integrationsalgorithmus[HOR69,RIS69], dem Programm für Grenzwerte und demIntegrationspogramm {\tx WANDERER} für definite Integrale [PROM11].Rationale Funktionen werden nach klassischen Verfahren integriert. Durch Aufteilung des Nenners und Partialbruchzerlegung werden die Brüche zerlegt und einfache Teilintegrale erzeugt. {\tx SIN} ist ein stark heuristisches Programm, das noch aus dem Jahre 1967 stammt [MOS67]. Der<font COLOR="0000FF">Risch</font>-Algorithmus wird zur Verarbeitung verschachtelterExponentiale und Logarithmen verwendet. Das Programm {\tx WANDERER} behandelt unter anderem auch Wegintegrale. </p> <p>{\tx MACSYMA} wird abgerundet durch eine Gruppe von Funktionen, die dem Nutzer die Arbeit mit seinen Funktionen erleichtern (z.B. ein Editor) und die ihn bei der Testarbeit unterstützen. </p> <p>&nbsp;</p> <h2>LISP als Implementationssprache</h2> <p>Ein wesentlicher Grund für die bleibende Aktualität von LISP liegt in seiner Eignung zur Implementation von Verarbeitungsprogrammen für Programmiersprachen. Von jeder Sprache für die nichtnumerische Informationsverarbeitung wird man mindestens erwarten, daß sich in ihr Syntaxanalysatoren schreiben lassen; die Verwendung dieser Programme in einem (Produktions-)Compiler ist eine andere Frage. </p> <p>Die prinzipielle Möglichkeit, mit LISP Compiler bzw. Interpreter zu schreiben, wurde schon in den frühesten Arbeiten über LISP angedeutet durch die Beschreibung der LISP-Verarbeitung durch ein LISP-Programm selbst [MCC60c]. Allerdings darf man in diesem Beispielnicht mehr sehen, als der Autor selbst es tat: Ein pädagogisches theoretisches Vehikel. </p> <p>Durch die Entwicklung des LISP-Assemblers (der Listen von listenförmigen Assemblerbefehlen zu Maschinenbefehlen umformt) wurde es möglich, die Teile eines Sprachübersetzers an den Syntaxanalysator anzuschließen, die bis dahin nicht und auch heute nur selten in einer höheren Sprache formuliert werden können: Codeerzeugung, Laden bzw. Verwalten von Maschinenprogrammen und Konvertieren höherer Datenstrukturen (hier der Listenstruktur) in die Rechnerwortstruktur. Eine erste Anwendung dieser Hilfsmittel wurde im ursprünglichen LISP1.5-Compiler vollzogen: Ein LISP-Programm transformiert andere LISP-Programme in Assemblerprogramme und übergibt diese dem LISP-Assembler. Der nun mögliche Sonderfall, daß der Compiler sich selbst übersetzt, wird <font COLOR="FF0000"> Bootstrapping</font> genannt (wir kletterneinen steilen Berg empor, indem wir uns abwechselnd auf die Schuhe treten und immer den unteren wieder wegziehen - im Deutschen denkt man mehr an Münchhausen) und stellt eine Anfang der sechziger Jahre durch LISP ins Gespräch gebrachte Neuheit dar. </p> <p>Der LISP-Compiler geht aber von bereits im Speicher befindlichen, in Form von Listenstrukturen aufgebauten Programmen aus [STO74]. Diesemüssen in der üblichen Quellsprache von LISP (manchmal {\em S-Sprache} genannt) formuliert und durch den Interpreter eingelesen worden sein. Durch die Formulierung der Eingabe- und Ausgabeprogramme sowie spezieller Hilfsfunktionen in der LISP-Assemblersprache wurde es möglich, die compilierten Programme auf externe Medien auszugeben und sie unabhängig von LISP-System in einen Rechner zu laden. Diese Möglichkeit machte man sich bei den ersten Übertragungen von LISP-Implementationen auf andere Rechner zunutze: Man schrieb zunächst Funktionen, die die Ausgaben des Compilers für andere Rechner lesbar machten. Dann wurde den Compiler so geändert, daß er Befehle erzeugte, die dem neuen Rechner entsprachen. Inzwischen hatte man die Basis des neuen LISP-Systems auf dem Zielrechner entwickelt: Unterprogrammverwaltung, wichtigste Basisfunktionen, Speicherplatzverwaltung. Alle übrigen Funktionen wurden in LISP formuliert, im Heimatrechner compiliert und in einem Format ausgegeben, das es möglicht machte, diese Teile zu den fertigen Programmteilen im Zielrechner hinzuzufügen. </p> <p>Auf diese Weise wurden die LISP-Systeme für den M460 [HART64a] undfür den Q-32 [SAU64b] erstellt: Im Fall des Q-32 bestand das gesamteProgramm aus etwa 4000 Karten, jeweils etwa die Hälfte in LISP bzw. in der Assemblersprache für den Q-32 geschrieben. Der LISP-Teil wurde auf der IBM 7090 compiliert und ergab etwa 6000 Karten Maschinencode. In dem Assemblerteil war ein Stück, mit Hilfe dessen die Ausgabe des Compilers eingelesen und dem übrigen System hinzugefügt worden ist. </p> <p>In LISP sind aber auch Funktionen enthalten, mit denen man eine zeichenweise Eingabe ausführen kann. Alle Zeichen werden in Atome umgewandelt, deren jeweiliger Name eben dieses Zeichen ist. Man kann nun aus sequentiellen Zeichenfolgen auf externen Medien (Lochkarten, Terminals usw.) interne Listen von Zeichen aufbauen. So könnte man einen Syntaxanalysator für eine beliebige Programmiersprache schreiben: Die Eingabeprogrammliste wäre diese lineare Zeichenliste. </p> <p>Mit Hilfe weiterer Funktionen kann man ausgewählte Teilfolgen dieser Zeichenliste zu LISP-Atomen konvertieren: Zeichenfolgen, die Namen entsprechen, zu normalen literalen Atomen, Zeichenfolgen, die Zahlen darstellen, zu ganzen oder Gleitkomma-Zahlen. Kurz, der Syntaxanalysator kann von den Aufgaben der lexikalischen Analyse entlastet werden [GRI71a]. Enthält das betreffende LISP-System etwa die {\ttREADLIST}-Funktion, so ist der Scanner (wie man den lexikalischen Analysator auch nennt) höchst einfach zu entwickeln: READLISTakzeptiert als Argument eine Liste von Atomen, betrachtet diese als Zeichen und liest so aus der Liste heraus, wie der normale Einleseprozeß vom externen Medium dies tun würde. Dadurch ist der Programmierer von der komplizierten Aufgabe wie Konstruktion von Gleitkomma-Zahlen aus Mantisse und Exponent entlastet; er muß nur die Anfänge und Enden der lexikalischen Einheiten erkennen und die einzelnen Zeichen in Listen zusammensammeln. Das übrige erledigt {\tt READLIST}. Besonders fortgeschrittene LISP-Systeme bieten variable Scanner an [QA72b, STO78].</p> <p>Auf der Basis eines solchen lexikalischen Analysators läßt sich eine Syntaxanalysemethode vorteilhaft anwenden, die auch sonst LISP besonders angemessen ist: Die des <font COLOR="FF0000">rekursiven Abstiegs</font> [GRI71a, KLE75](engl. recursive descend). Hierbei ist im Syntaxanalysator für jedes Nichtterminal eine rekursive Funktion vorhanden, die die Phrasen verarbeitet, die diesem Sprachelement entsprechen. Die Funktion beginnt ihre Arbeit, wenn sicher ist, daß eine solche Phrase beginnt. Sie ruft andere Funktionen auf, wenn die ihr entsprechende Produktion in der Sprachdefinition auf der rechten Seite mehrere Nichtterminale enthält. Der Syntaxbaum (eine Listenstruktur) wird aus den Werten aufgebaut, die die einzelnen Funktionen liefern. </p> <p>Die typische Anwendung dieses Vorgehens liegt dann vor, wenn der Syntaxbaum als LISP-Programm konstruiert ist, das dem Quellprogramm entspricht. Auf dieser Art kann der nach dem Verfahren des rekursiven Abstiegs arbeitende Syntaxanalysator als Transformator von der höheren Sprache in LISP angesehen werden. Fast alle auf LISP aufbauenden höheren Sprachen für die Künstliche Inteligenz bzw. Formelmanipulation ({\tx MLISP} [SM70], {\tx MLISP2} [SM73a], {\txREDUCE} [HEA73], {\tx SCRATCHPAD} [GRI71b], {\tx MACSYMA} [BOG75]usw.) bedienen sich dieser Methode. </p> <p>Das übliche Prinzip der lexikalischen Analyse wird bereichert durch das Konzept der <font COLOR="FF0000"> Einlesemakros</font>. Hierbei kann es sich um ganznormale Zeichenkettenmakros handeln, die einen Ersetzungsmechanismus aktivieren. Eine andere Variante ist das in LISP erfundene {\em Makrozeichen}: Mit einem Zeichen kann ein Verarbeitungsprogramm verknüpft sein, das z.B. die Analyse der darauffolgende Zeichen steuert bzw. das Ergebnis der lexikalische Analyse beeinflußt. </p> <p>Sehr beliebt als Makrozeichen sind die Präfixe für Variablen in den Musterbeschreibungen. So wird etwa die Zeichenkette \$?x in{\tx MICROPLANNER} [SUS71] umgesetzt in den Term (THV X). Dieweitentwickelten LISP-Systeme wie INTERLISP [TE74] und MACLISP [MOO74]bieten die Makrozeichen auch dem normaler LISP-Nutzer während der Eingabe seiner LISP-Programme. Eine ganze Gruppe von höheren Sprachen für die Künstliche Intelligenz unterscheidet sich von der Basissprache LISP (in der Syntax) nur durch die Verwendung dieser Präfixe (daneben natürlich durch neue Funktionen und Verwaltungsmechanismen). Beispiele sind {\tx MICROPLANNER} [SUS71],{\tx QA4} [RUL72] und {\tx QLISP} [SAC76].</p> <p>Da die Syntaxanalysatoren in LISP geschrieben sind, ist es leicht, schon während der Analyse von Eingabezeichen einer höheren Sprache Teile des erzeugten LISP-Programmn auszuführen und mit ihm das Syntexanalyseprogramm zu verändern bzw. zu vervollständigen. Auf diese Weise sind fast alle Ideen, die im Zusammenhang zu den {\em erweiterbaren Sprachen} stehen, in LISP implementierbar (vgl.[SO74]).</p> <p>Am weitesten entwickelt wurden die Ideen zur Ausnutzung der Sprachverarbeitungsmöglichkeiten von LISP in dem Compiler-Compilersystem {\tx MLISP2} [SM73A]. Die zu verarbeitendeProgramiersprache wird mittels einer Metasprache für die Syntax und mit semantischen Funktionen beschrieben. {\tx MLISP2} generiert ein vollständiges Verarbeitungsprogramm, wobei Backtracking-Prinzipien verwendet werden. </p> <p>Die günstige Basis, die LISP für die Verarbeitung von Programmiersprachen bietet, wurde nicht nur für die Einbettung höherer Sprachen in LISP verwendet, sondern erleichterte auch die Erstellung von Systemen zur Programmverifikation (vgl. Abschnitt 2.5). Für die Verarbeitung anderer formaler Sprachen (z.B. Beweisüberprüfer {\tx FOL} [WEY74]) und der natürlichen Sprache ist diese Anwendung vonLISP natürlich auch sehr wichtig. </p> <p>&nbsp;</p> <h2>Andere Anwendungen in der Künstlichen Intelligenz</h2> <p>LISP war von <font COLOR="0000FF">McCarthy</font> als Basissprache für die Entwicklung vonProgrammen, die künstliche Intelligenz zeigen sollten, konzipiert worden. So reduziert sich die Anwendung nicht auf die bisher erwähnten Gebiete. Aus dem vielfältigen Rest sollen einige besonders anschauliche Einsatzgebiete erwähnt werden. </p> <p>&nbsp;</p> <h3>Robotersteuerung </h3> <p>LISP wird für die Steuerung von Robotern verwendet. Obwohl die Echtzeit-Steuerung der Augen (Fernsehkameras) und Hände (Manipulatoren) in anderen Sprachen (Assenblersprache, FORTRAN. SAIL [RES76]) programmiert wird, so dient LISP zur ``intellektuellen'' Kontrolleund <font COLOR="FF0000">Planung</font> der Roboter-Aktionen. Pläne sind dabei Folgen vonAktionen oder Operationen, mit denen beabsichtigt wird, einen Anfangszustand in der Umwelt des Roboters in einen Zielzustand überzuführen [SAC73,SAC75].</p> <p>Die Pläne werden als Baumstrukturen dargestellt: Man kann sie zerteilen in die Unterzielstruktur und den Graph, der die logischen Relationen zwischen den Entscheidungen repräsentiert, die bei der Planerstellung getroffen wurden [SAC75][S.181].</p> <p>Meist wurden die die Pläne konstruierenden Programme nicht direkt in LISP aufgestellt, sondern in höheren, auf LISP aufbauenden Sprachen. Typische Beispiele hierfür sind {\tx PLANNER} [HEW71c], {\txCONNIVER } [MCD72], {\tx QA4} [RUL72], {\tx QLISP} [SAC76] und{\tx SOUP} [SAC75].</p> <p>Eine typische Vorgehenweise findet sich in [RUL72]: Die Aktionenwerden in Listenform notiert, die Daten bzw. das `Wissen' über die Roboterumwelt in P-Listen-Strukturen (vgl. Abschnitt 4.7). So lautet etwa ein Plan für die Bewegung eines Roboters durch eine Tür in {\tx QA4} [RUL72][S.293]: (GOTHRUDOOR (LAMBDA (INROOM (TUPLE ROBOT- M)) (PROG (DECLARE X K L) (IF (NOT $ONFLOOR) THEN (FAIL)) (EXISTS (CONNECTS -K -L $M)) (GOAL $GO (INROOM ROBOT $L)) (GOAL $GO (NEXTTO ROBOT $K)) (MAPC (QUOTE (TUPLE (AT ROBOT -X) (NEXTTO ROBOT-X))) $DELETE) (ASSERT (INROOM ROBOT $M)) ($BUILD (`(: $GOTHRUDOORACTIONACTION $K)))))) Der Plan ähnelt sehr einem LISP-Programm. Der Leser lasse sich nicht durch die Präfixe \$ und - verwirren: Sie haben besondere Bedeutungbeim Mustervergleich und lösen Bedingungsoperationen aus -- wenn etwa eine Tür gesucht wird, die den Raum M mit dem Ort, an dem sichder Roboter befindet (das ist K), verbindet.</p> <p>Zunächst wird geprüft, ob der Roboter wirklich auf dem Fußboden steht. Ist das nicht der Fall, dann versagt das Programm (FAIL). Dann wird ein Weg gesucht, der den Ort, an dem derRoboter ist, mit dem Raum M verbindet. Die Suche in derDatenbasis wird durch die Ausdrücke durchgeführt, die Unterziele (GOAL) realisieren. Dabei kann es sein, daß der Zustand derDatenbasis, der dem geforderten Ort des Roboters (an der Tür {\tt K}, im Raum L) entspricht, erst durch Bewegung des Roboterserzeugt werden muß. Ist der Zustand nachgewiesen, dann wird die Bewegung vorbereitet: Die alte Ortsbeschreibung wird gelöscht ({\tt DELETE)} und die neue in die Datenbasis eingetragen (ASSERT).Zum Schluß wird dann das Echtzeit-Steuerprogramm aufgerufen, das die wirkliche Aktion hervorruft. </p> <p>Sowohl der MIT-Roboter [WINS72] als auch der des SRI [RA69] waren aufdiese Art mit dem LISP-System gekoppelt. </p> <p>&nbsp;</p> <h3>Programmerzeugung</h3> <p>Wenn Pläne dieser Art in LISP erzeugt werden, dann lassen sich auch Programme generieren. Hier gibt es verschiedene Möglichkeiten: Man kann in LISP Programmgeneratoren schreiben, die Programme in LISP selbst oder in anderen Programmiersprache erzeugen; man kann Programmoptimierer entwickeln, die vorgegebene Programme verbessern oder umorganisieren. Man kann Compiler schreiben, die aus Programmen höherer Ebene (Spezifikationen, deklarativen Programmen) Programme niederer Ebene (mehr prozeduraler Natur) ableiten. So erlaubt etwa das in LISP geschriebene Formelmanipulationssystem REDUCE [HEA73] dem Nutzer, nachdemalle symbolischen Umformungen erledigt sind, ein FORTRAN-Programm zu erzeugen, das die dem symbolischen Ergebnis entsprechenden numerischen Berechnungen durchführt. </p> <p>Wie entscheidend derartige Fähigkeiten in einem Programm sein können, zeigt das Beispiel eines Programmsystems für die Berechnung elektrischer Netzwerke [ELS77]: Der Nutzer gibt eine Beschreibung desNetzwerks und die gewünschten Analyseschritte ein, und das Programm erzeugt ein lauffähiges FORTRAN-Programm für die Lösung der Netzwerkgleichungen. Da außerdem nach symbolischen Differentiationsschritten auch für die <font COLOR="0000FF">Jacobi</font>-Matrix einberechnendes Programm erzeugt wird, können die Autoren ihr System mit folgender Behauptung anbieten: ``...Damit können für eine große Klasse von speziellen Netzwerken Gleichungssyteme erzeugt werden, die in ihrer Effizienz mit handgeschriebenen vergleichbar sind...'' ([ELS77],S.102). Heute werden ähnliche hybride Methoden insbesondere bei der Anwendung von Finite-Element-Methoden genutzt. </p> <p>In diesem Fall wird dem Programmgenerator eine Beschreibung des Netzwerks übergeben.... </p> <p>Programme auf Grund allgemeinerer Vorgaben zu generieren, ist inzwischen ein stark bearbeitetes Forschungsgebiet geworden [AD75]. Mankann je nach der Informationsquelle für das Wissen über das zu erzeugende Programm die Ansätze aufteilen [SIK75] in Versuche,Programme zu generieren unter der Verwendung von Beschreibungen der Eigenschaften (sowohl mit Hilfe einer Programmiersprache als auch mit Hilfe logischer Kalküle), in Versuche, bei der Erzeugung von Abarbeitungsprotokollen auszugehen und schließlich in Versuche, dabei Beispiele (d.h. Eingabe-Aussage-Wertpaare) als Basis zu benutzen.\footnote{Stoyan} </p> <p>Von diesen Ansätzen sind wohl nur zwei natürlich und zukunftsträchtig: Die Beschreibung von Eigenschaften des gewünschten Algorithmus mit Hilfe einer formal logischen Spezifikationen [WAL75] unddie Angabe von exemplarischen Beispielen. </p> <p>Das Programm {\tx EXAMPLE} [SHAW75] von <font COLOR="0000FF">D.E.Shaw</font>, <font COLOR="0000FF"> D.R.Swartout</font> und <font COLOR="0000FF">C.C.Green</font> akzeptiert z.B. folgendeInformationen und gibt bei der Generierung folgende Fragen bzw. Vermutungen aus: </p> <p>\begin{tabular} {ll} $\leftarrow$ &amp; WHAT SHALL I CALL THE TOP-LEVEL FUCTION?\\$\rightarrow$ &amp; PAIRREVERSE.\\$\leftarrow$ &amp; OK! NOW TYPE IN AN EXAMPLE ARGUMENT LIST!\\$\rightarrow$ &amp; ((a b c d e f )).\\$\leftarrow$ &amp; AND WHAT WOULD BE THE VALUE OF PAIRREVERSE WITH THIS\\&amp; ARGUMENT LIST ?\$\rightarrow$ &amp; (b a d c f e).\\$\leftarrow$ &amp; OK. I'LL TRY.\\$\leftarrow$ &amp; DOES PAIRREVERSE ((C D E F )) = (D C F E) ?\\$\rightarrow$ &amp; YES.\\$\leftarrow$ &amp; I HAVE DEFINED PAIRREVERSE AS FOLLOWS:\\\end{tabular} </p> <p>(PAIRREVERSE (LAMBDA (ARG1) (COND ((NULL ARG1) NIL) ((NULL (CDR ARG1)) NIL) (T (APPEND (LIST (CAR (CDR ARG1)) (CAR ARG1)) (PAIRREVERSE (CDR (CDR ARG1)))))))) Wenn auch die bisher erzielten Resultate sich auf eng begrenzte Aufgabenklassen beziehen, deuten sich doch interessante Möglichkeiten an. Einige Beispiele und vielleicht doch eine grobe Beschreibung der Programmfunktionen sollten die Erzeugung relativ komplizierter Programme ermöglichen. </p> <p>Wichtig für die Erzeugung von Programmen ist Spezialwissen auf dem Fachgebiet, in dem das Problem liegt, das mit dem erstrebten Programm gelöst bzw. algorithmiert werden soll. Ein derartiger Ansatz [LEN75]liegt vor, scheint aber noch nicht zur Realisierung gediehen zu sein. </p> <p>&nbsp;</p> <h3>Wissenbasierte Systeme</h3> <p>Neues Wissen zu lernen, Wissen zu speichern und verfügbar zu machen, sind unstreitig zentrale Probleme der Künstlichen Intelligenz. So nehmen unter den gegenwärtigen Anwendungsbeispielen von Methoden dieses Spezialgebiets auch Systeme einen besonderen Platz ein, die bei Anfragen auf Grund einer <font COLOR="FF0000">Wissensbasis</font> mögliche Antworten generierenund mittels Schlußregeln die wahrscheinlichste aussondern. </p> <p>Da bei diesen Systemen die Frage nach der Erforschung von Deduktionsprozeduren oder bestmöglicher Wissensrepräsentation nicht gestellt wird, sondern nach einer Grundsatzentscheidung eine Basis für die Anwendung aufgebaut wird, nennt man diese Systeme nach dem Hauptaspekt ihrer Verwendung <font COLOR="FF0000">wissens-basierte Systeme</font> (engl. knowlegde based systems, systems showing expert knowledge). </p> <p>Schon heute gibt es wissensbasierte Systeme, die über der einen derartigen Umfang von Allgemein- und Spezialwissen verfügen, daß sie auch für Wissenschaftler interessante Hilfsmittel sind. Gedacht sind die meisten von ihnen für Fachleute, die kein Spezialwissen auf dem Gegenstandsbereich besitzen und im Dialog Auskünfte einholen bzw. mit Hilfe des wissensbasierten Systems Fragen beantworten. </p> <p>Zu den bedeutenderen Systemen gehörten Ende der siebziger Jahre {\tx DENDRAL}, {\tx MYCIN}, {\tx AM}, und auch das bereits erwähnte {\tx LUNAR} (vgl. Abschnitt 3.2) paßt in diese Reihe. </p> <p>{\tx DENDRAL} sagt chemische Strukturformeln für Substanzen voraus, für die spektrometrische Daten vorliegen [BUC68,BUC69,BUC76,BUC77,MIC74]. {\tx MYCIN} stellt Diagnosen über Infektionskrankheiten und gibt Empfehlungen zur medikamentösen Behandlung [SHO75,SH76]. {\txAM} entdeckt interessante Begriffe in der elementaren Mathematik [LEN77]. Während {\tx AM} inzwischen problematisiert wird, dient das1978 aufgegebene {\tx MYCIN} immer noch als Paradebeispiel für ein Expertensystem. Dabei scheint eine wirkliche Anwendung nie stattgefunden zu haben, obwohl verschiedene Tests bezüglich der Diagnose- und Therapiequalität des Systems stattgefunden haben. Besonders einflußreich war die Art, eine Regelsprache durch einen entsprechenden Interpreter (``Inferenzmaschine'') in LISP zu implementieren, das Subsystem zur Generierung von Erklärungen, deren wesentlichste Komponente ein Übersetzer aus der Regelsprache in die englische Sprache war, sowie das <font COLOR="FF0000"> Wissensakquisitionssystem</font> {\tx THEREISIAS},das Regeln aus dem Englischen in die Regelsprache übersetzte, sie in das Regelprogramm einordnete und beim Testen Unterstützung bereitstellte. </p> <p>{\tx DENDRAL} ist dabei das älteste (seit 1965) und inzwischen meistbenutzte (?) System dieser Art. Neben den Daten vom Massenspektrometer und vom Kernresonanzspektrometer kann der Nutzer auch aus anderen Quellen gewonnene Informationen als Einschränkungen und Hinweise zur Verfügung stellen. </p> <p>Das System generiert in einem ersten Schritt, ausgehend von den Meßdaten, wahrscheinliche (bzw. unwahrscheinliche) Teilstrukturen der chemischen Verbindung. Diese können später bei der Überlegung bezüglich der Gesamtstruktur praktisch als Einheiten angesehen werden und vermindern so drastisch die Komplexität. Für jede Art von Meßdaten existiert ein Programmteil, der für den Strukturgenerator (den 2. Schritt) durch Verringerung des Suchraums gewissermaßen strategische Regeln entwirft. </p> <p>Im 2. Schritt werden dann alle plausiblen Strukturen erzeugt. Dabei werden aus den topologisch möglichen Strukturen diejenigen ausgesondert, welche mit den vom Nutzer gelieferten Einschränkungen nicht verträglich sind. Durch die bereits (aus dem 1. Schritt) gegebenen Teilstrukturen werden bei weitem nicht soviel generiert, wie zunächst legal wären. </p> <p>Schließlich werden alle nun vorliegenden Kandidatenstrukturen bezüglich ihrer Plausibilität untersucht, eine Rangordnung wird hergestellt und die Menge durch Einführung einer unteren Ranggrenze verkleinert. ...welche Art von Meßdaten zu erwarten wären, wenn die Substanz solcherart aufgebaut wäre. Diese Hypothesen werden mit den wirklichen Meßdaten verglichen. Die beste Erklärung der gegebenen Daten wird dann ausgewählt und als Vorschlag ausgegeben. </p> <p>{\tx DENDRAL} soll um 1980 von vielen Chemikern täglich benutzt worden sein. Schon 1969 bestand das Programm erfolgreich den folgenden Test: Prof. <font COLOR="0000FF"> Djerassi</font> von der Stanford Universität stellte den Teilnehmernseines Forschungsseminars die Aufgabe, drei Massenspektren zu interpretieren. Die Teilnehmer (Doktoranden und Diplomanden) bekamen die Spektren, die chemische Summenformel und die Information, daß es sich um azyklische Strukturen handle. Die erste Aufgabe wurde vom Programm und einem Diplomanden gelöst, die zweite nur vom Programm (zwei Diplomanden hatten die Lösung unter einer Menge von Vorschlägen) und die letzte konnte auch das Programm nicht lösen (ein anwesender Doktor der Chemie lieferte zwei Vermutungen, unter denen die richtige Lösung war). Dabei benötigte das Programm 2 bis 5 Minuten, die Chemiker jedoch 16 bis 45. </p> <p>Nicht unwesentlich für dieses Programmsystem ist die vorteilhafte Art, wie die chemischen Strukturen durch Listenstrukturen dargestellt werden können. </p> <p>Weitere ähnliche Systeme sind {\tx MOLGEN} [STEF77]und {\tx CRYSALIS} [ENG77] für die Planung genetischer Experimentebzw. zur Voraussage von Proteinstrukturen aus Verteilungen der Elektronendichte, wie sie aus röntgenkristallographischen Daten gewonnen werden. </p> <p>Inzwischen soll eine große Menge solcher Expertensysteme existieren. Manchmal hört man unglaubliche Zahlen bezüglich des Ausmaßes ihrer Anwendung in den USA. Im überblickbaren Deutschland ist die Zahl deutlich geringer. </p> <h3>Anwendungen in Sprach- und Musikwissenschaft</h3> <p>Typisch nichtnumerische Informationsverarbeitung ist auszuführen, wenn es um die Analyse von musikalischen Partituren oder um die Verwendung philosophischer Grundbegriffe in den Werken großer Philosophen geht. </p> <p><font COLOR="0000FF">S.Smolliar</font> entwickelte ein musiktheoretisches Analyseprogramm,das auf den Theorien <font COLOR="0000FF">H. Schenkers</font> beruhte\footnote{die in Europa längst nicht so aktuell sind wie in den USA}. Es ist verbunden mit dem interpretierenden Programm {\tx EUTERPE} [SMO66], das durch einLISP-Programm gesteuert wird [SMO67] und die Musik spielt. Der Vorteildieses Programms ist, daß bei der Analyse auch hierarchische Strukturen, die in einer Komposition angelegt sind, berücksichtigt werden (andere rechnergestützte Systeme zur Musikanalyse betrachten die musikalische Information als Zeichenkette). Die Forscher hofften, daß auch Komponisten sich des Programms bedienen werden [FRA76].</p> <p><font COLOR="0000FF">B.G.Greenberg</font> hat um 1983 ein oft vorgeführtes Musikprogramm auf einerSymbolics-LISP-Maschine geschrieben. Es verarbeitete eine musikalische Sprache, mit der <font COLOR="0000FF">Greenberg</font> nicht nur Noten, Tempi, Rhytmen, Lautstärkenvariationen u.ä. vom Komponisten vorgeschriebene Ausdruckselemente darstellte, sondern auch subjektiv begründete Ausdrucksparameter. Der Musik-Compiler steuerte eine Orgelsimulation, in der die Konfigurationen bekannter Orgeln nachgebildet wurden, mit der möglichen Online-Modifikation der Registerwahl u.ä. </p> <p><font COLOR="0000FF">Y.Wilks</font>' Analyse des Gebrauchs philosophischer Grundbegriffe[WILK73] versucht, die oftmals nicht klar definierbare Verwendung vonKategorien in philosophischen Werken (<font COLOR="0000FF">Plato, Spinoza</font>) undinsbesondere die Ausnutzung der Mehrdeutigkeit für die Argumentation nachzuweisen. </p> <p>Der wesentliche Unterschied zwischen Anwendungen der nichtnumerischen Informationsverarbeitung in der Naturwissenschaft und in der Musik- und der Sprachwissenschaft kommt in diesen Andeutungen zum Ausdruck: Während es nur ein Problem der Kenntnis und Vollständigkeit ist, die theoretischen Resultate der Naturwissenschaften für die Programmierung nutzbar zu machen, stehen sich auf dem Gebiet der Sprach- und der Musik-Wissenschaften oft Theorien gleichranging gegenüber, die nur Teilaspekte (oft verschiedene) erfassen. </p> <p>&nbsp;</p> <h3>Computerspiele</h3> <p>Die Verwendung von Rechnern als Spielpartner gehört zu einer der frühesten Benutzung von Ideen der Künstlichen Intelligenz. Spiele sind deshalb besonders gut als Anwendungsbeispiele geeignet, weil sie sich in vielen Fällen einfach beschreiben lassen, weil man sich bei dieser Beschreibung meist formaler Methoden bedienen kann, weil dadurch das schwierige Problem der natürlichen Sprache und gleichzeitig das Problem des Allgemeinwissens über eine komplexe Welt ausgeklammert werden können und dennoch genügend schwierige Situationen auftreten. </p> <p>Ein typisches und sicher das Paradebeispiel ist seit jeher das Schachspiel. Mindestens seit 1955 [NEW58], spätestens nach 1960 wurdenverschiedene Schachprogramme geschrieben. Viele davon sind in Maschinensprachen einigermaßen effizient; andere sind in höheren Sprachen geschrieben und dienen zum Studium von Strategieverhalten, des Lernens aus vergangenen Partien und aus Fehlern und zum experimentieren mit Baumsuchverfahren. Das in LISP geschriebene Sprachprogramm von {\sc Greenblatt} [GREL67], {\tx MacHack}, war eines der einflußreichenProgramme. Alljährlich werden in den USA Landesmeisterschaften der Schachprogramme ausgetragen. Auch anläßlich der IFIP-Konferenzen finden internationale Meisterschaften in Computerschach statt. Mitte der siebziger Jahre machte ein russisches Schachprogramm von <font COLOR="0000FF">Arlasarow</font> und <font COLOR="0000FF"> Donskoi</font> aus Moskau[BOT66,AD70] Furore (allerdings nicht in LISP geschrieben).</p> <p>Unter den anderen in LISP geschriebenen Spielprogrammen ist ein Goprogramm von <font COLOR="0000FF">B.Wilcox</font> [RET75] erwähnenswert, in demdie topologischen Strukturen des Go-Spiels mittels Listenstrukturen nachgebildet werden. </p> <p>end &#26;</plaintext></li> </font></font> </BODY></HTML>