LbP Prädikatenlogik
Aus ProgrammingWiki
Wiki-Quelltext dieser Seite.
<language>Prolog</language>
==Logik und Programmierung==
===Aussagenlogik===
Eine ''Aussage'' ist ein Satz, der entweder wahr oder falsch ist. Man spricht auch von einer zweiwertigen Logik. Dabei kommt es nicht darauf an, dass eine den Satz beurteilende Person zu einem gegebenen Zeitpunkt weiss, ob der Satz wahr ist oder nicht (Interpretation). Entscheidend ist die Zuordnung genau eines ''Wahrheitswertes'' (entweder <math>\text{wahr}</math> oder <math>\text{falsch}</math>; niemals beides, niemals keines) zu einem Satz.
Aussagen enthalten keine Variablen. Es ist etwas ganz anderes, wenn wir Variablen benutzen, um damit Aussagen zu bezeichnen, so wie man das für andere Werte in vielen Bereichen der Mathematik ebenfalls tut. Aussagenvariablen werden benutzt, um insbesondere komplexe Aussagen übersichtlich darzustellen und mit ihnen rechnen zu können. Dabei werden die Variablen mit Wahrheitswerten belegt.
Komplexe Aussagen werden aus Aussagen (einfache und komplexe) zusammengesetzt. Dafür stehen Verknüpfungsoperatoren (Junktoren) zur Verfügung:
*eine einstellige Operation: die Negation <math>\neg</math>
*die zweistelligen Operationen
**Konjunktion <math>\wedge</math>
**Disjunktion <math>\vee</math>
**Subjunktion <math>\to</math>
**Bijunktion. <math>\leftrightarrow</math>
Neben den Definitionen dieser Operationen, sind Bindungsverhältnisse (Vorrangbeziehungen) und Klammersetzungen zu berücksichtigen, wenn man für eine konkrete Belegung der aussagenlogischen Variablen den Wert eines zusammengesetzten Ausdrucks bestimmen möchte.
Manchmal fragt man auch umgekehrt nach der sog. ''Erfüllungsmenge'': Für welche Belegungen wird eine vorgegebene (komplexe) Aussage wahr? Mit der Frage nach der Erfüllungsmenge begibt man sich in den metasprachlichen Bereich, d.h. wir formulieren Aussagen über solche Aussagen, deren Aufbau wir gerade definiert haben. Die Sprache der Ausdrücke nennen wir Objektsprache, die Sprache, in der wir über Ausdrücke sprechen, heisst ''Metasprache''.
Auch die Frage nach der ''Allgemeingültigkeit'' einer Aussage <math>A</math> ist eine metasprachliche Formulierung: <math>A</math> ist allgemeingültig, wenn <math>A</math> für alle Belegungen wahr wird. Beispielsweise ist leicht zu zeigen, dass <math>x\vee\neg x</math> für alle Belegungen von <math>x</math> wahr wird, d.h. die angegebene Aussage <math>A</math> ist allgemeingültig, und man schreibt allgemein <math>A\Leftrightarrow\text{wahr}</math>.
Zwei Aussagen <math>A</math> und <math>B</math> nennt man ''äquivalent'', kurz <math>A\Leftrightarrow B</math>, wenn <math>A\leftrightarrow B\Leftrightarrow \text{wahr}</math> ist. Diese Schreibweise hebt den metasprachlichen Unterschied zwischen der Bijektion <math>\leftrightarrow</math> und der Äquivalenz <math>\Leftrightarrow</math> hervor.
Eine wichtige Ordnungsrelation für Aussagen ist die ''Implikation'' <math>\Rightarrow</math>. <math>A\Rightarrow B</math> gilt genau dann, wenn <math>A\to B\Leftrightarrow\text{wahr}</math>.
Es gibt eine Reihe aussagenlogischer Regeln, die äquivalente Umformungen von Ausdrücken gestatten, ohne die Äquivalenz durch Betrachtung aller Belegungen nachweisen zu müssen. Häufig benutzt man ein ''DeMorgansches Gesetz'' <math>\neg(A\wedge B)\Leftrightarrow\neg A\vee\neg B</math> oder Regeln für das aussagenlogische Schliessen, wie etwa die Abtrennungsregel (modus ponens): <math>A\wedge (A\to B)\Rightarrow B</math>.
===Prädikatenlogik===
Der entscheidende Unterschied zur Aussagenlogik ist die Hinzunahme von ''Variablen'' zu Aussagen, so dass ''Aussageformen'' entstehen. Ansonsten gelten die gleichen Junktoren wie oben. In Analogie zur Aussagenlogik verwendet man Symbole, um Prädikate zu benennen.
Die ''Belegung von Variablen'' in prädikatenlogischen Ausdrücken erfolgt mit Werten aus wohldefinierten Grundmengen. Beispielsweise wird das einstellige Prädikat "<math>x</math> ist teilbar durch 3", kurz <math>P(x)</math>, durch die natürlichen Zahlen <math>0,3,6,9,\dots</math> erfüllt.
Eine Variable in einem prädikatenlogischen Ausdruck darf nur dann mit einem konkreten Wert belegt werden, wenn sie nicht im Einflussbereich eines ''Quantors'' steht. Anders ausgedrückt: Quantoren binden Variablen und machen eine Aussageform zur Aussage, wenn keine freien Variablen vorkommen. Es gibt den ''Allquantor'' <math>\forall</math> und den ''Existenzquantor'' <math>\exists</math>. Dann liest man das für natürliche Zahlen <math>i,n</math> definierte Prädikat <math>\forall n(3\mid n\Leftrightarrow\exists i(3i=n))</math>
folgendermassen. Für alle <math>n</math> gilt: <math>3</math> teilt <math>n</math> genau dann, wenn es ein <math>i</math> derart gibt, dass <math>3i=n</math>. Die Aussageform <math>\forall n(3\mid n\leftrightarrow\exists i(3i=n))</math> muss für alle Belegungen von <math>n</math> wahr werden, um allgemeingültig zu sein. Es reicht also nicht aus, ein oder zwei Werte für <math>n</math> auszuprobieren. Dies macht die Sache schwierig! Die Berechnung des Wahrheitswertes ist also nicht immer ohne Weiteres möglich, denn wir müssten unendlich viele Fälle untersuchen.
In der ''Prädikatenlogik erster Stufe'', kurz PK(1) für ''Prädikatenkalkül 1. Ordnung'', können nur die genannten Variablen quantifiziert werden. In der zweiten Stufe quantifiziert man ausserdem Prädikatenvariablen.
Aus der theoretischen Informatik ist bekannt, dass die Prädikatenlogik ''aufzählbar'' aber ''nicht entscheidbar'' ist. Mit anderen Worten: Es gibt keinen Algorithmus, der für jede beliebige vorgegebene Aussage in endlicher Zeit entscheidet, ob sie aus einer Menge geltender Aussagen (Axiomsystem) ableitbar ist oder nicht.
===PK(1), HORN-Klausel-Logik und Prolog===
Eine Teilmenge der Prädikatenlogik, die die Entscheidbarkeit garantiert, ist die ''Hornklausellogik''. PROgramming in LOGig (Prolog) basiert darauf.
Eine Klausel ist eine Disjunktion negierter und nichtnegierter logischer Ausdrücke. Darin enthaltene Variablen <math>x_j</math> sind ''grundsätzlich universell quantifiziert'', d.h. im Einflussbereich von <math>\forall</math>-Quantoren. Die Allquantoren werden aber nicht extra angegeben.
<math>\neg A_1\vee\neg A_2\vee\ldots\vee\neg A_m\vee B_1\vee B_2\vee\ldots\vee B_n</math>
Wendet man die Rechengesetze der Prädikatenlogik an, nämlich <math>\neg X\vee\neg Y\Leftrightarrow\neg (X\wedge Y)</math> und <math>\neg G\vee H\Leftrightarrow G\Rightarrow H</math>, so erhält man den dazu äquivalenten Ausdruck <math>A_1\wegde A_2\wegde\ldots\wegde A_m\Rightarrow B_1\vee B_2\vee\ldots\vee B_n,\text{ mit } n,m\geq 0</math>.
Jeder prädikatenlogische Ausdruck kann in eine äquivalente Konjunktion von Klauseln übertragen werden.
''Hornklauseln'' haben eine eingeschränkte Klauselgestalt: Die Disjunktion darf nur höchstens einen unnegierten Ausdruck enthalten, d.h. <math>\neg A_1\vee\neg A_2\vee\ldots\vee\neg A_m\vee B</math> oder äquivalent dazu
<math>B\Leftarrow A_1\wedge A_2\wedge\ldots\wedge A_m, m\geq 0</math>.
<math>B</math> gilt, wenn <math>A_1</math> und <math>A_2</math> usw. und <math>A_m</math> gelten. Unter Benutzung von Hornklauseln können Aussagen effizient abgeleitet werden. Die zugehörige ''Prolog-Klausel'' lautet:
<math>B :- A_1, A_2, ..., A_m</math>.
Jede Klausel obiger allgemeiner Gestalt kann in eine Hornklausel transformiert werden. Unnegierte Aussagen müssen ggf. doppelt negiert werden, z.B. <math>\neg(\neg A)</math>. Um es ganz deutlich zu sagen: Jeder prädikentlogische Ausdruck kann in einen äquivalenten Hornklauselausdruck übertragen werden.
Dabei ergibt sich allerdings ein Problem, denn die Negation erweist sich als ein sog. ''Metaprädikat'', also ein Prädikat, dessen Argument ein Prädikat ist. Dies verstösst gegen die logische Grundlage von Prolog. Der Preis für diesen Verstoss wird weiter unten an einem Beispiel illustriert. Im Allgemeinen ist die Fehleranfälligkeit eines Prologprogramms bei kontrolliertem Einsatz der Negation gering.
''Prozedural'' gedeutet, wird ein Beweisziel <math>B</math> berechnet, indem alle Aussagen <math>A_1</math> bis <math>A_m</math> berechnet werden. Dieser Prozess setzt sich ''rekursiv'' solange fort, bis man passende variablen-freie Klauseln (Axiome) in der Datenbasis findet.