Aussagenlogik Flashcards
(19 cards)
Definition Aussagenlogik
In der Aussagenlogik werden Aussagen über logische Operatoren verknüpft. Der Satz „die Straße ist nass“ ist eine Aussage, genauso wie „es regnet“. Diese beiden Aussagen lassen sich nun verknüpfen zu der neuen Aussage “wenn es regnet ist die Straße nass”
Definition Syntax
Syntax 2.2 - Man liest die Operatoren und Symbole folgendermaßen
Semantik - Beispiel für Wahrheitswerte
Starten wir mit einem Beispiel und fragen uns, ob die Formel A ^ B wahr ist. Die Antwort heißt: Es kommt darauf an, ob die Variablen A und B wahr sind. Steht zum Beispiel A für „Es regnet heute.“ und B für „Es ist kalt heute.“ und dies trifft beides zu, so ist A ^ B wahr. Steht jedoch B für „Es ist heiß heute.“ (und dies trifft nicht zu) so ist A ^ B falsch.
Wir müssen offenbar den Aussagevariablen Wahrheitswerte zuordnen, die Zuständen der Welt entsprechen.
Semantik 2.3 Definition
Definition der logischen Operatoren per Wahrheitstabelle
Für die erlaubten Basisoperatoren definieren wir nun deren Wahrheitswerte, indem wi in der Wahrheitstabelle für alle möglichen Belegungen einen Wahrheitswert angeben.
Bindungsregeln
¬ bindet stärker als ∧
∧ bindet stärker als ∨
∨ bindet stärker als ⇒
Um die Äquivalenz von Formeln klar von der syntaktischen Äquivalenz zu unterschei- den, definieren wir:
Die semantische Äquivalenz wird vor allem dazu dienen, in der Metasprache, das heißt der natürlichen Sprache, über die Objektsprache, nämlich die Logik, zu reden. Die Aussa- ge „A B“ etwa besagt, dass die beiden Formeln A und B semantisch äquivalent sind. Die Aussage „A , B“ hingegen ist ein syntaktisches Objekt der formalen Sprache der Aussagenlogik.
Je nachdem, in wievielen Welten eine Formel wahr ist, teilt man die Formeln ein in folgende Klasse
Eine Formel heißt
- erfüllbar, falls sie bei mindestens einer Belegung wahr ist.
- allgemeingültig oder wahr, falls sie bei allen Belegungen wahr ist. Wahre Formeln heißen auch Tautologien.
- unerfüllbar, falls sie bei keiner Belegung wahr ist.
Jede erfüllende Belegung einer Formel heißt Modell der Formel.
Wahrheitstafel für komplexere Formeln
Definition Beweisverfahren
In der KI sind wir daran interessiert, aus bestehendem Wissen neues Wissen herzulei- ten, beziehungsweise Anfragen zu beantworten. In der Aussagenlogik geht es darum zu zeigen, dass aus einer Wissensbasis WB, das heißt einer (eventuell umfangreichen) aussagenlogischen Formel, eine Formel Q2 folgt. Zuerst definieren wir den Begriff der Folgerung.
immer dann, wenn WB wahr ist, ist auch Q wahr.
Q steht für Query (Anfrage)
Deduktionstheorem
Wiederspruchsbeweis
Beweisverfahren Kalkül
Eine Möglichkeit, das Durchprobieren aller Belegungen bei der Wahrheitstafelmethode zu vermeiden, ist die syntaktische Manipulation der Formeln WB und Q durch Anwen- dung von Inferenzregeln mit dem Ziel, diese so stark zu vereinfachen, dass man am Ende sofort erkennt, dass WB ˆ Q. Man bezeichnet diesen syntaktischen Prozess als Ab- leitung und schreibt WB ` Q.
Um sicherzustellen, dass ein Kalkül keine Fehler macht, definieren wir zwei fun- damentale Eigenschaften von Kalkülen.
Die Korrektheit eines Kalküls stellt also sicher, dass alle abgeleiteten Formeln tatsäch- lich semantische Folgerungen aus der Wissensbasis sind. Der Kalkül produziert keine „falschen Folgerungen“. Die Vollständigkeit eines Kalküls hingegen stellt sicher, dass der Kalkül nichts übersieht. Ein vollständiger Kalkül findet immer einen Beweis, wenn die zu beweisende Formel aus der Wissensbasis folgt. Ist ein Kalkül korrekt und vollständig, so sind syntaktische Ableitung und semantische Folgerung zwei äquivalente Relationen
Resolutionskalkül
Der Resolutionskalkül zum Beweis der Unerfüllbarkeit von Formeln in konjunktiver Normalform ist korrekt und vollständig. Das heißt, für jede unerfüllbare Formel kann man mit Resolution die leere Klausel herleiten und umgekehrt.
Angehensweise zur Lösung einer Aufgabe in der Resolution
Zur Lösung derartiger Aufgaben geht man in drei Schritten vor: Formalisierung, Trans- formation in Normalform und Beweis
Hornklauseln
SLD Resolution
ür das backward chaining auf Hornklauseln wird SLD-Resolution verwendet. SLD steht für „Selection rule driven linear resolution for definite clauses“
SLD-Resolution spielt in der Praxis eine wichtige Rolle, denn Programme in der Lo- gikprogrammiersprache Prolog bestehen aus prädikatenlogischen Hornklauseln, und ihre Abarbeitung erfolgt mittels SLD-Resolution (siehe Aufgabe 2.13, bzw. Kap. 5).
