1 Einleitung
In der ersten Phase der KI-Forschung war die Suche nach allgemeinen Problemlösungsverfahren wenigstens in der formalen Logik erfolgreich. Dort wurde ein mechanisches Verfahren angegeben, um die logische Allgemeingültigkeit von Formeln zu beweisen. Das Verfahren konnte auch von einem Computerprogramm ausgeführt werden und leitete in der Informatik das automatische Beweisen ein (Mainzer 2019, Kap. 3).
Der Grundgedanke ist einfach zu verstehen. In der Algebra werden Buchstaben x, y, z, … durch Rechenoperationen wie z. B. Addieren (+) oder Subtrahieren (–) verbunden. Die Buchstaben dienen als Leerstellen (Variablen), um Zahlen einzusetzen. In der formalen Logik werden Aussagen durch Variablen A, B, C, … bezeichnet, die durch logische Junktoren wie z. B. ‚und‘ (∧), ‚oder‘ (∨)‚wenn-dann‘ (→), ‚nicht‘ (¬) verbunden werden. Die Aussagenvariablen dienen als Leerstellen, um Aussagen einzusetzen, die entweder wahr oder falsch sind. So ist z. B. A ∧ B eine logische Formel, die durch Einsetzung der wahren Aussagen 1+3=4 für A und 4=2+2 für B in die wahre Aussage 1+3=4 ∧ 4=2+2 übergeht. In der Arithmetik ergibt sich daraus der wahre Schluss 1+3=4 ∧ 4=2+2 → 1+3=2+2 (vgl. Artikel über Grundlagen des logischen Schließens). Allgemein ist aber der Schluss A ∧ B → C nicht wahr. Demgegenüber ist der Schluss A ∧ B → A logisch allgemeingültig, da für die Einsetzung von beliebigen wahren oder falschen Aussagen für A und B sich immer eine wahre Gesamtaussage ergibt.
2 Erfüllbarkeit und Resolutionsmethode
Der Beweis für die Allgemeingültigkeit eines logischen Schlusses kann in der Praxis sehr kompliziert sein. Daher schlug John A. Robinson 1965 die sogenannte Resolutionsmethode vor, nach der Beweise nach dem Muster logischer Widerlegungsverfahren gefunden werden können (Robinson 1965; Richter 1978, S. 185 ff.; Schöning 1987, S. 85 ff.). Man startet also mit der Annahme des Gegenteils (Negation), d. h. der logische Schluss sei nicht allgemeingültig. Im nächsten Schritt wird dann gezeigt, dass alle möglichen Anwendungsbeispiele dieser Annahme zu einem Widerspruch führen. Es gilt also das Gegenteil der Negation und der logische Schluss ist allgemeingültig. Die Robinsonsche Resolutionsmethode benutzt logische Vereinfachungen, wonach man jede logische Formel in eine sogenannte konjunktive Normalform umwandeln kann. In der Aussagenlogik besteht eine konjunktive Normalform aus negierten und nicht negierten Aussagenvariablen (Literale), die durch Konjunktion (∧) und Disjunktion (∨) verbunden sind.
Bei der konjunktiven Normalform (¬A ∨ B ) ∧ ¬B ∧ A besteht die Formel aus den Konjunktionsgliedern (Klauseln) ¬A ∨ B, ¬ B und A, die durch die Konjunktion ∧ verbunden sind. In diesem Beispiel folgt aus den Konjunktionsgliedern ¬A ∨ B und ¬B logisch das Literal ¬A. (Der Grund ist einfach: Aus ¬B folgt, dass ¬A ∨ B nur wahr werden kann, wenn ¬A wahr ist.) Aus ¬A und dem restlichen Konjunktionsglied A folgt im nächsten Schritt die immer falsche Aussageform ¬A ∧ A und damit der Widerspruch ⊡ („leeres Wort“):
Mechanisch besteht das Verfahren also darin, widersprechende Teilaussagen aus Konjunktionsgliedern einer logischen Formel zu streichen („Resolution“) und diese Prozedur mit den entstehenden „Resolventen“ und einem entsprechenden anderen Konjunktionsglied der Formel zu wiederholen, bis ein Widerspruch (die „leere“ Klausel, die nie wahr werden kann) abgeleitet werden kann.
In einem entsprechenden Computerprogramm terminiert dieses Verfahren für die Aussagenlogik. Es zeigt also in endlicher Zeit, ob die vorgelegte logische Formel allgemeingültig ist. Allerdings wächst die Rechenzeit nach den bisher bekannten Verfahren exponentiell mit der Anzahl der Literale einer Formel. Was nun die „Künstliche Intelligenz“ betrifft, so können Computerprogramme mit der Resolutionsmethode automatisch über die Allgemeingültigkeit logischer Schlüsse wenigstens in der Aussagenlogik im Prinzip entscheiden. Menschen hätten große Schwierigkeiten, bei komplizierten und langen Schlüssen den Überblick zu bewahren. Zudem sind Menschen wesentlich langsamer. Mit steigender Rechenkapazität können Maschinen also wesentlich effizienter diese Aufgabe des logischen Schließens erledigen.
ein allgemeingültiger Schluss der Prädikatenlogik.
Für die Formeln der Prädikatenlogik lässt sich ebenfalls ein verallgemeinertes Resolutionsverfahren angeben, um wieder aus der Annahme der allgemeinen Ungültigkeit einer Formel einen Widerspruch abzuleiten. Dazu muss eine Formel der Prädikatenlogik ähnlich wie in der Aussagenlogik (aber deutlich komplizierter) in eine Normalform gebracht werden, aus deren Klauseln sich mechanisch ein Widerspruch ableitet lässt. Falls die Formel tatsächlich widersprüchlich ist, kommt das Verfahren auch in endlicher Zeit zu diesem Ergebnis. Allgemeingültigkeit kann man gleichermaßen in endlicher Zeit nachweisen, da in diesem Fall die Negation der Formel widersprüchlich ist (es gibt kein Gegenbeispiel). Allerdings gibt es einen dritten Fall in dem die Formel in manchen Anwendungsfällen wahr ist und in anderen falsch, je nachdem wie man die Individuen und Prädikate interpretiert („mit Leben füllt“). Daher kann es in der Prädikatenlogik (im Unterschied zur Aussagenlogik) vorkommen, dass das Resolutionsverfahren kein Ende findet. Das Computerprogramm läuft dann unbegrenzt weiter. Es kommt dann darauf an, Teilklassen zu finden, in denen das Verfahren nicht nur effizient läuft, sondern überhaupt terminiert. Maschinelle Intelligenz kann zwar die Effizienz von Entscheidungsprozessen steigern und sie beschleunigen. Sie ist aber auch (wie menschliche Intelligenz) den prinzipiellen Grenzen logischer Entscheidbarkeit unterworfen.
3 Geschichtliche Entwicklung des automatischen Beweisens
Die Schule um den Mathematiker David Hilbert hatte in den 1920er-Jahren gezeigt, dass Prädikatenlogik die „Sprache der Mathematik“ ist, d. h. dass mathematische Konzepte in Prädikatenlogik formuliert werden können. Gleichzeitig hatte die mathematische Logik ein (zunächst sehr theoretisches) Verfahren entwickelt, um die Allgemeingültigkeit (bzw. Widersprüchlichkeit) einer Formel mechanisch nachzuweisen. Eine Formel kann nur dann widersprüchlich sein, wenn es ein endliches Anwendungsbeispiel gibt, das den Widerspruch aufzeigt. Außerdem gibt es zu jeder Formel ein „allgemeinstes“ (i.A. unendlich großes) Anwendungsbeispiel.
Dieses nach dem Logiker Jacques Herbrand benannte Beispiel besteht aus aussagenlogischen Formeln, die man systematisch und sukzessiv aus den in der Formel vorkommenden Symbolen konstruieren kann. Diese Formeln stellen generische Namen dar für Individuen, die in einem beliebigen Anwendungsbeispiel nach Maßgabe der prädikatenlogischen Formel notwendigerweise vorkommen müssen. Jeder endlich große Anfang des Beispiels stellt nun eine Konjunktion von aussagenlogischen Formeln dar, deren Erfüllbarkeit (oder Widersprüchlichkeit) man mit rein aussagenlogischen Mitteln in endlicher Zeit entscheiden kann (z. B. trivialerweise mit Wahrheitstabellen).
Mit der Verfügbarkeit von Computern in den 1950er-Jahren begannen mehrere Forscher in den USA das genannte Beweisverfahren konkret auszuformen und auf verschiedene Arten zu implementieren. Das Kernproblem war dabei, zunächst ein effizientes Verfahren für die aussagenlogische Erfüllbarkeit (SAT-Solving) zu finden, die wiederholt für endliche Anfänge des kombinatorisch stark anwachsenden Herbrand Beispiels nachzuweisen war.
Willard V. O. Quine hatte dazu Wahrheitstabellen vorgeschlagen, die aber exponentielles Wachstum aufweisen (Quine 1955). Paul Gilmore hatte stattdessen eine disjunktive Form der Art (A∧B∧C … ∨ E∧F∧G … ∨…) benutzt und auf einer IBM 704 implementiert, aber auch dieser Ansatz war schon auf kleinen Beispielen ineffizient (Gilmore 1960). Die Firma IBM produzierte von 1954 bis 1960 das Modell 704 mit Schaltkreisen aus Röhren, etwa 18KB bis 144KB Hauptspeicher aus Magnetkernen sowie Magnetbandspeicher von je 5MB. Martin Davis und Hilary Putnam fassten 1960 in einer auch heute noch sehr lesenswerten Arbeit im Journal of the ACM die Gesamtsituation zusammen und präsentierten zudem ein völlig neues Verfahren für die Erfüllbarkeitsprüfung, das im Kern auf der (später so bezeichneten) Idee der Resolution aufbaut (Davis und Putnam 1960). Sie konnten damit von Hand ein Beispiel von Gilmore rechnen, bei dem dessen Programm abbrechen musste.
Danach implementierten Davis, Logemann und Loveland das neue Verfahren ebenfalls auf einer IBM 704 und entdeckten sofort, dass es an einer entscheidenden Stelle verändert werden musste, um nicht ebenfalls ein explosives Wachstum der Formeln auszulösen. In ihrer 1962 publizierten Arbeit wird der heute als „DPLL“ bekannte rekursive Algorithmus zum Suchen einer erfüllenden Variablenbelegung beschrieben, der erstmalig ein praktikables Verfahren zum SAT-Solving darstellt und bis in die 1990er-Jahre hinein Bestand hatte (Davis et al. 1962). Das Beispiel von Gilmore wurde damit in nur zwei Minuten automatisch gelöst.
Im Jahr 1965 publizierte John A. Robinson eine neue Methode zum Beweisen in Prädikatenlogik (Robinson 1965). Dieses „Resolution“ genannte Verfahren erlaubt es, direkt aus der Menge der prädikatenlogischen Klauseln neue logisch implizierte Klauseln abzuleiten, ohne wie zuvor einen Umweg über die Aussagenlogik zu nehmen. Falls die ursprüngliche Formel (bzw. deren Klauselmenge) widersprüchlich ist, kann man immer in endlicher Zeit die „leere“ Klausel ableiten, die nicht erfüllt werden kann und so den Widerspruch zu Tage treten lässt. Die aussagenlogische Variante wurde bereits oben demonstriert. Prädikatenlogisch ist die Sache komplizierter, denn die beiden Klauseln {P(x)} und {¬P(f(y))} widersprechen sich auf den ersten Blick noch nicht. Allerdings sind x und y implizit als allquantifiziert zu verstehen, sodass aus ∀x.P(x) auch ∀x.P(f(x)) folgt und damit ein Widerspruch zu ¬P(f(y)).
Zum Vergleich: in der „alten“ Methode aus den 1950er-Jahren hätte man den Widerspruch durch sukzessives und im Prinzip zielloses Aufbauen des Herbrand-Beispiels wie folgt ermitteln müssen: Soll es ein nicht-leeres Beispiel geben, so muss mindestens ein Individuum „a“ vorhanden sein und es muss eine Funktion „f“ geben. Damit muss es auch ein „f(a)“ geben, und weiter „f(f(a))“, „f(f(f(a)))“, usf. Wir prüfen nun, ob durch Einsetzen von a (in x und y) alleine ein Widerspruch zu Tage tritt; das ist nicht der Fall. Auch durch Einsetzen von a für x und f(a) für y ergibt sich kein Widerspruch. Erst durch Einsetzen von f(a) für x und a für y tritt der Widerspruch zu Tage. Durch geschicktes Einsetzen kommt man also (viel) schneller zum Ziel als durch ungeschicktes Einsetzen, und nach jedem Einsetzen braucht man eine erneute Erfüllbarkeitsprüfung. Demgegenüber vergleicht Robinson die prädikatenlogischen Formeln systematisch und stellt die Gleichheit durch gezieltes Einsetzen („Unifikation“) her. Im Beispiel sehen wir, dass wir im alten Verfahren für x ein Individuum „f(a)“ einsetzen müssen, wenn wir für y „a“ einsetzen, oder eben für x ein „f(f(a))“ und für y dann ein „f(a)“ etc.
Prädikatenlogische Resolution ist deutlich effizienter als das vorhergehende Verfahren; die Gilmore Formel wird nach nur 6 einfachen Resolutionsschritten (Ableitung neuer Klauseln) als widersprüchlich erkannt, was auch von Hand problemlos zu bewältigen ist. Im Gegenzug waren die ersten 24 Einsetzungen (endlich großen Anfänge, s.o.) von Davis und Putnam jeweils erfüllbar, und erst die 25. Einsetzung erzeugte einen Widerspruch (in 75 Klauseln).
Aufgrund der deutlich besseren Effizienz wendete sich die damalige KI sofort der Resolutionsmethode als neuem Werkzeug für das zentrale Problem des „Reasoning“ (Herstellen von Schlussfolgerungen) zu. Ein unabhängig agierender intelligenter Akteur oder Agent muss seine Umwelt wahrnehmen können, daraus Schlussfolgerungen für sein intendiertes Handeln ableiten und diese sodann in Aktionen übersetzen. Hieraus ergaben sich Teilgebiete der KI wie Bilderkennung („Computer Vision“) und Sprachverstehen einerseits und Robotik andererseits sowie als zentrale Komponente Wissensrepräsentation mit intelligentem Schlussfolgern und Planen. Nach der herkömmlichen wissenschaftlichen Methode modelliert man die Umwelt mathematisch, um durch Berechnungen Vorhersagen treffen können. Da die Mathematik (nach Hilbert) im Kern prädikatenlogisch gefasst werden kann, liegt es nahe, eine prädikatenlogische Repräsentation und einen automatischen Beweiser als zentrales Werkzeug vorzusehen.
Schon im Jahr 1971 publizierte Nils Nilsson vom Stanford Research Institute SRI das einflussreiche Buch „Problem solving methods in AI“ (Nilsson 1971), vgl. auch (Nilsson 1980; Genesereth und Nilsson 1989). Neben verschiedenen Algorithmen um Gewinnstellungen in Lösungsräumen z. B. von Brettspielen zu suchen, widmen sich 3 von 8 Kapiteln dem Automatischen Beweisen mit der Resolutionsmethode und ihren Anwendungsmöglichkeiten. Hier geht es nun nicht mehr nur um den effizienten Beweis eines logischen Widerspruchs, sondern vor allem auch um die Extraktion von konkreten Handlungsanweisungen und Antworten aus dem Widerspruchsbeweis. Ein Beispiel ist die Extraktion eines Plans zum Erfüllen eines Ziels bis hin zum automatischen Schreiben eines Programms.
Eine eingeschränkte Form von Klauseln (sog. Horn-Klauseln) wurden zur Grundlage der neuen Programmiersprache PROLOG (s.u.). Grundidee ist hier, sowohl Daten als auch Berechnungsregeln als Menge von Klauseln zu schreiben und einen universellen Beweiser für die konkreten Berechnungen zu nutzen. Dies sollte transparente, leicht wartbare Programme ermöglichen ohne die Notwendigkeit komplexer Schleifenkonstrukte und Verzweigungen. Einer der ersten Prolog Compiler wurde um 1978 am „Department for Artificial Intelligence“ der Universität Edinburgh fertiggestellt (Clocksin und Mellish 1981).
In Deutschland begann eine kleine Gruppe um Jörg Siekmann, damals Assistent an der Universität Karlsruhe (heute KIT), mit der Programmierung eines Resolutionsbeweisers; ein Ziel sollte es sein, die Beweise in einem Lehrbuch der Berechnungstheorie automatisch nachzuvollziehen. Diese Gruppe organisierte 1983 die führende Tagung „International Joint Conference of AI (IJCAI-83)“ in Karlsruhe. Themen waren System Support, Theorem Proving, Cognitive Modelling, Automatic Programming, Planning and Search, Knowledge Representation, Learning and Knowledge Acquisition, Logic Programming, Natural Language, Expert Systems, Vision, Robotics.
Aber in Deutschland war die KI noch nicht wirklich etabliert. Einen eigenen Fachbereich gab es dafür anders als in Edinburgh nicht; erst 1988 wurde das Deutsche Forschungszentrum KI (DFKI) gegründet. Ein führendes Lehrbuch der Informatik sprach noch von der „sogenannten künstlichen Intelligenz“. Allerdings erwiesen sich viele kühne Ziele der KI auch als ungemein schwieriger als zunächst vermutet. Nicht nur scheint Intelligenz doch ein unerwartet komplexes (und leistungsfähiges) Phänomen zu sein. Auch schon mathematische Logik und ihre Beweise sind nicht einfach zu bewältigen, besonders wenn dies effizient und in nützlicher Frist geschehen soll. Bereits 1962 hatten Davis, Logemann und Loveland resümiert: „We hoped that some mathematically meaningful and, perhaps nontrivial, theorems could be solved. The actual achievements in this direction were somewhat disappointing“ (Davis et al. 1962, S. 395).
Zwischenzeitlich war das SAT-Solving der Aussagenlogik etwas in Vergessenheit geraten, da es ja für Beweise in der Prädikatenlogik nicht mehr gebraucht wurde. Dies blieb im Wesentlichen bis Mitte der 1990er-Jahre so. Dann aber wurden mikroelektronische Schaltungen immer komplexer, deren Schaltpläne im Wesentlichen in Boole’scher Algebra (Schaltalgebra) vorliegen. Ein weit publiziertes Ereignis war 1994 ein (seltener) Fehler in der Gleitkommadivision des Pentium 5 Prozessors der Firma Intel. Im Zuge des neu erwachten Interesses an der Verifikation kombinatorischer Schaltkreise gelang Joao Marques-Silva (1995) und seinem Betreuer Karem Sakallah 1996 ein wesentlicher und richtungsweisender konzeptioneller Durchbruch beim SAT-Solving: die intelligente Kombination der DPLL Suchprozedur mit dem Deduktionsverfahren der (aussagenlogischen) Resolution zum conflict driven clause learning CDCL (Marques-Silva und Sakallah 1996, 1999).
Deduktionsverfahren häufen ständig neues Wissen an, indem sie dynamisch neue Klauseln erzeugen und leiden in der Folge unter hohem Speicherverbrauch. Reines DPLL-Suchen hat keinen dynamischen Speicherbedarf, kann aber unter langen Laufzeiten leiden, wenn es durch backtracking wiederholt auf dieselbe Weise bei der Lösung derselben Teilmenge von Formeln scheitert. Das CDCL Verfahren besteht nun darin, dass man aus den Konflikten lernt, auf die man bei der DPLL Suche stößt. Ein Konflikt besteht darin, dass eine der Klauseln unter der momentan untersuchten Variablenbelegung falsch (false) wird. Dieser Fall tritt niemals direkt durch eine true/false Entscheidung auf, sondern immer durch weitere Wertepropagationen aufgrund einer Entscheidung.
Solche Propagationen werden immer durch Klauseln erzwungen: z. B. erzwingt eine Klausel {x, y} die Propagation von y=true sobald x=false gesetzt wird. Falls eine Klausel false wird, so liegt das daran, dass sie die umgekehrte Propagation erzwingen würde, im Beispiel etwa {x, ¬y}. In dieser Situation gibt es aber immer eine Resolvente, im Beispiel wäre das {x}. Als Resolvente ist die Klausel eine logische Konsequenz der zu lösenden Formel und kann als zusätzliche Klausel „gelernt“ werden. In unserem Beispiel würde sie verhindern, dass nach backtracking jemals wieder eine Lösung mit x=false versucht wird, denn {x} erzwingt zuvor sofort x=true.
Eine in der Praxis ungeheuer wichtige Konsequenz des CDCL Solving besteht darin, dass der Solver im Fall einer unlösbaren Formel nun die leere Klausel „lernt“ und dazu einen Resolutionsbeweis konstruiert. Nun kann das bislang lapidare Ergebnis „UNSAT“ durch einen nachvollziehbaren (und unabhängig nachprüfbaren) Beweis begründet werden. In Fällen, wo „UNSAT“ auf einen Fehler in der Anwendung (z. B. einem Schaltkreis) zeigt, kann aus dem Beweis oft eine Anleitung zur konkreten Lokalisation des Fehlers und zu seiner Korrektur entnommen werden.
Neben dem Lernen wurden für moderne CDCL Solver weitere wichtige Komponenten entwickelt, wie z. B. hoch effiziente Implementierungen der Wertepropagation und gute Heuristiken zur Auswahl der nächsten zu belegenden Variable. Außerdem entstanden um das CDCL-Solving weitere verwandte Algorithmen wie die Berechnung von Primimplikanten (wichtig für die Minimierung von Formeln) oder zur Berechnung maximaler lösbarer Teilmengen von unlösbaren Klauselmengen (wichtig für Optimierungszwecke). Einen umfassenden Überblick gibt das Handbook of Satisfiability (Biere et al. 2009).
Einige wesentliche industrielle Anwendungsgebiete für das SAT-Solving sind heute die formale Verifikation von Mikroelektronik und von Software sowie die Lösung von Konfigurationsproblemen. Im Falle von Software übersetzt man ein Programm vollautomatisch in eine Boolesche Formel. Im Falle von Konfigurationsproblemen (z. B. plugin Konfiguration im Eclipse Programm-Editor) codiert man die Randbedingungen („wenn A dann nur wenn auch B aber nicht C oder D“) als Klauseln und lässt den Solver eine gültige Konfiguration berechnen. Auch den Konfiguratoren der Automobilindustrie, die man im Internet benutzen kann, liegen ähnliche Randbedingungen zugrunde. Viele Automobilhersteller benutzen heute SAT-Solver um ihre hochkomplexen Konfigurationsprobleme zu lösen bzw. die Formelsysteme zu analysieren und zu validieren (Küchlin und Sinz 2000; Sinz et al. 2003), Kap. „Symbolische KI für die Produktkonfiguration in der Automobilindustrie“. In der Mikrobiologie bestehen Anwendungsmöglichkeiten dadurch, dass sowohl Proteine als auch Gene durch die Kombination von endlich vielen Grundbausteinen gebildet werden, was man durch Boolesche Variablen codieren kann.
Moderne CDCL Solver funktionieren äußerst effizient und robust, ohne händische Hilfen, und bewältigen Anwendungsprobleme mit (Hundert-)Tausenden von Variablen und Klauseln. Da das Erfüllbarkeitsproblem ein NP-vollständiges Problem ist (es ist das prototypische NP-vollständige Problem) ist kein Algorithmus bekannt, der es auch im verzwicktesten Fall in weniger als exponentieller Zeit (in der Anzahl der Variablen) löst; außerdem ist die Existenz eines solchen Algorithmus sehr unwahrscheinlich. Andererseits können somit auch alle anderen NP-vollständigen Probleme im Kern durch SAT-Solver gelöst werden (Knuth 2016; Thomason 2018; Bringsjord et al. 2018).
Insgesamt gibt es viele wichtige Anwendungsprobleme, bei denen die Struktur der Klauseln ein praktisch effizientes CDCL Solving erlaubt. Selbst wenn also durch die KI Forschung auf dem Gebiet des Reasoning bis jetzt nicht alle Erwartungen und Hoffnungen erfüllt werden konnten, so hat schon alleine das daraus entstandene SAT-Solving zu vielen konkreten Anwendungen in Industrie und Wissenschaft geführt.
4 KI-Programmiersprachen
Grundlage der symbolischen KI sind Programmiersprachen, die aus formalen Kalkülen der Logik und Mathematik entwickelt wurden.
4.1 KI-Programmiersprache Prolog
Um ein Problem mit einem Computer zu lösen, muss das Problem in eine Programmiersprache übersetzt werden. So war FORTRAN eine der ersten Programmiersprachen, bei denen ein Programm aus einer Folge von Befehlen an den Computer besteht wie z. B. „springe an die Stelle z im Programm“, „schreibe in die Variable x den Wert a“. Im Zentrum stehen Variablen, also maschinentechnisch Register- bzw. Speicherzellen, in denen Eingabewerte gespeichert und verarbeitet werden. Wegen der eingegebenen Befehle spricht man auch von einer imperativen Programmiersprache.
In einer prädikativen Programmiersprache wird demgegenüber Programmierung als Beweisen in einem System von Tatsachen aufgefasst. Diese Wissensdarstellung ist aus der Logik wohlvertraut. Eine entsprechende Programmiersprache heißt „Programming in Logic“ (PROLOG), die seit Anfang der 1970er-Jahre in Gebrauch ist (Kowalski 1979; Hanus 1986; Schefe 1987, S. 285 ff.). Grundlage ist die Prädikatenlogik, die wir schon im vorherigen Abschnitt kennengelernt haben. Wissen wird in der Prädikatenlogik als Menge von wahren Aussagen dargestellt. Um Wissensverarbeitung geht es in der KI-Forschung. Daher wurde PROLOG zu einer zentralen Programmiersprache der KI.
wobei „NAME“ ein beliebiger Name einer Relation ist. Zeichenfolgen, die in der syntaktischen Form von Fakten wiedergegeben werden, heißen Literale.
Aufgrund einer vorgegebenen Wissensbasis in Form von Literalen können in PROLOG Lösungen einer Frage bzw. Problemstellung nach der Resolutionsmethode gefunden werden.
4.2 KI-Programmiersprache LISP
Alternativ zu Aussagen und Relationen lässt sich Wissen auch durch Funktionen und Zuordnungen wie in der Mathematik darstellen. Funktionale Programmiersprachen fassen daher Programme nicht als Systeme von Tatsachen und Schlussfolgerungen (wie PROLOG) auf, sondern als Funktionen von Mengen von Eingabewerten in Mengen von Ausgabewerten. Während prädikative Programmiersprachen an der Prädikatenlogik orientiert sind, gehen funktionale Programmiersprachen auf den λ-Kalkül zurück, den Alonzo Church 1932/33 zur Formalisierung von Funktionen mit Rechenvorschriften definierte (Church 1941). Ein Beispiel ist die funktionale Programmiersprache LISP, die von John McCarthy bereits Ende der 1950er-Jahre während der ersten KI-Phase eingeführt wurde (McCarthy et al. 1960; Stoyan und Goerz 1984). Daher ist sie eine der ältesten Programmiersprachen überhaupt und war von Anfang an mit dem Ziel der Künstlichen Intelligenz verbunden, menschliche Wissensverarbeitung auf die Maschine zu bringen. Wissen wird dabei durch Datenstrukturen dargestellt, Wissensverarbeitung durch Algorithmen als effektive Funktionen.
- 1)
Ein Atom ist ein s-Ausdruck.
- 2)
Wenn x und y s-Ausdrücke sind, dann auch (x.y).
- 1)
NIL („leere Symbolfolge“) ist eine Liste.
- 2)
Wenn x ein s-Ausdruck und y eine Liste ist, dann ist der s-Ausdruck (x.y) eine Liste.
vereinfacht zu (S1 S2 … SN). Listen können wieder Listen als Elemente enthalten, was den Aufbau sehr komplexer Datenstrukturen erlaubt.
Wendet man diese Funktionen auf Listen an, so liefert also CAR das erste Element, CDR die restliche Liste ohne das erste Element. CONS ergibt eine Liste mit dem ersten Parameter als erstes Element und dem zweiten Parameter als Rest.
Baumdarstellungen (a) der Liste (S1 S2 … SN) und (b) des s-Ausdruck (A.((B.(C.NIL)))). (Quelle: eigene Darstellung)
Oft ist aber auch sinnvoll, Listen als (geordnete) Mengen von Symbolen aufzufassen. So macht es wenig Sinn (14235) als Anwendung der Funktion 1 auf die Argumente 4, 2, 3, 5 zu lesen, wenn es um eine Sortierungsaufgabe der Zahlen geht. In LISP wird daher das Symbol QUOTE eingeführt, wonach die folgende Liste nicht als Funktionsanweisung, sondern als Aufzählung von Symbolen zu verstehen ist: z. B. QUOTE(14235) oder kurz ’(14235). Dann ist nach Definition z. B. CAR’(123) = 1, CDR’(123) = ’(23) und CONS1’(23) = ’(123). Während Variable durch literale Atome notiert werden, können nicht-numerische Konstanten durch Quotierung von Variablen unterschieden werden: z. B. die Variablen x und LISTE und die Konstanten ’x und ’LISTE.
Dabei sind P1, P2, …, PN die formalen Parameter der Funktion, NAME ist die Bezeichnung der Funktion. Der s-Ausdruck heißt Rumpf der Funktion und beschreibt die Funktionsanwendung mit den formalen Parametern. Wenn in einem Programm die Funktion NAME in der Form NAME (A1 A2 … AN) auftritt, dann sind im Rumpf der Funktion die formalen Parameter P1, P2, …, PN durch die entsprechenden aktuellen Parameter A1, A2, …, AN zu ersetzen und der so veränderte Rumpf auszuwerten.
Die Funktionsanweisung DREI’(415) ersetzt im Rumpf der Funktion DREI die formalen Parameter durch (CAR(CDR(CDR ’(415)))). Die Auswertung liefert dann den Wert 5 als drittes Element der vorgelegten Liste.
Falls die i-te Bedingung (1≤i ≤ N) den Wahrheitswert T und alle vorhergehenden Bedingungen den Wert NIL liefern, ist das Ergebnis des bedingten Ausdrucks der i-te s-Ausdruck. Der bedingte Ausdruck erhält den Wert NIL, falls alle Bedingungen den Wert NIL haben.
Die erste Bedingung stellt fest, ob die Liste leer ist. In diesem Fall hat sie die Länge 0. Die zweite Bedingung geht davon aus, dass die Liste nicht leer ist. In diesem Fall wird die Länge der Liste berechnet, in dem zur Länge der um das erste Element verkürzten Liste (LENGTH(CDR LISTE)) die Zahl 1 hinzu addiert wird.
Wir definieren nun, was allgemein unter einem LISP-Programm zu verstehen ist:
In den durch Punkte angedeuteten Rümpfen der verwendeten Funktionen können alle bisher definierten Funktionen verwendet werden. Da also ein LISP-Programm selber wieder ein s-Ausdruck ist, haben Programme und Daten in LISP die gleiche Form. Deshalb kann LISP auch als Metasprache für Programme auftreten, d. h. in LISP kann über LISP-Programme gesprochen werden. Eine weitere Eignung von LISP für Probleme der Wissensverarbeitung in der KI ist dadurch gegeben, dass eine flexible Verarbeitung von Symbolen und Strukturen möglich ist. Numerische Berechnungen sind nur Spezialfälle.
In der KI wird versucht, Problemlösungsstrategien algorithmisch zu strukturieren und sie dann in eine KI-Programmiersprache wie LISP zu übersetzen. Ein zentraler KI-Anwendungsbereich sind Suchprobleme. Wenn z. B. ein Gegenstand in einer großen Menge gesucht wird und kein Wissen über einen Lösungsweg des Problems zur Verfügung steht, dann werden auch Menschen einen heuristischen Lösungsweg wählen, der als British-Museum-Algorithmus bekannt ist.
- 1)
Es gibt eine Menge von formalen Objekten, in der die Lösung enthalten ist.
- 2)
Es gibt einen Generator, d. h. ein vollständiges Aufzählungsverfahren für diese Menge.
- 3)
Es gibt einen Test, d. h. ein Prädikat, das feststellt, ob ein erzeugtes Element zur Problemlösungsmenge gehört oder nicht.
Wenn die zu untersuchende Menge SET leer ist,
dann Misserfolg,
sonst
sei ELEM das nächste Element aus SET;
Wenn ELEM Zielelement,
dann liefere es als Lösung,
sonst wiederhole diese Funktion
mit der um ELEM verminderten Menge SET.
An diesem Beispiel wird deutlich: Menschliches Denken muss nicht unbedingt Vorbild für eine effiziente maschinelle Problemlösung sein. Ziel ist vielmehr, die Schnittstelle Mensch-Maschine mit einer ausdrucksstarken KI-Programmiersprache zu optimieren. Ob diese Sprachen mit ihren Datenstrukturen auch kognitive Strukturen des menschlichen Denkens simulieren bzw. abbilden, ist Thema der Kognitionspsychologie. KI-Programmiersprachen werden primär als computergestützte Werkzeuge zur optimalen Problemlösung eingesetzt.