Für was ist ein Beweiskalkül wichtig
deklarative Programmiersprachen –> AI
Was ist eine Wissenbasis WB?
bspw. mathematische Regeln, Spielregeln etc.
Kann durch einen logischen Term WB beschrieben werden.
Was ist Q?
Query, Anfrage –> Logischer Term
Logischer Term Q folgt aus Wissenbasis, wenn
alle Interpretationen von Q mit WB übereinstimmen
Wie nennt man Überprüfung mittels Wahrheitstabelle?
Semantische Folgerung
Wie nennt man Überprüfung mittels Manipulation an den Termen nach bestimmten Regeln ohne Wahrheitswerte einzusetzen?
Syntaktische Ableitung
Zwei Möglichkeiten, wie man semantisch überprüfen kann.
Deduktionstheorem: Wenn WB implikation Q allgemeingültig also Tautologie ist.
Widerspruchsbeweis –> WB und nicht Q = F also Kontradiktion
Was ist der Nachteil bei normaler Semantischer Folgerung?
Bei grosser Anzahl aussagenlogischer Variablen sehr lange Rechenzeit (SAT-Problem)
Welchen Vorteil hat der Widerspruchsbeweis?
Sobald True kann abgebrochen werden und es ist somit klar, dass es keine Semantische Folgerung ist.
Welche Regel ist eine der wichtigsten Ableitungsregeln in der Informatik?
Resolutionsregel
Zeichen Semantische Folgerung
Zeichen Syntaktische Ableitung
Resolutionsregel vereinfacht
Resolutionsregel durchführen, was beachten?
Nur eine Streichung pro Schritt, da es der Algorithmus auch nicht anders könnte.
Jede aussagenlogische Wissensbassis WB kann immer in… geschrieben werden.
Konjunktiver Normalform (KNF)
Konjunktive Normalfrom –>
Wissensbasis WB –> UND Verbindungen
Klausel K –> ODER Verbindungen
Literal L –> aussagenlogische Variablen oder Negation
Kalkül =
Büchlein von Ableitungsregeln
Beweiskalkül =
Gesamtheit der Regeln von syntaktischer Ableitung
Mögliche Eigenschaften von Beweiskalkül
- korrekt
- vollständig
Eigenschaft von Beweiskalkül: korrekt
Eigenschaft von Beweiskalkül: vollständig
Gödelscher Vollständigkeitssatz
Für die Prädikatenologik erster Stufe gibt es vollständige und korrekte Beweiskalküle
Gödelscher Unvollständigkeitssatz
Für die Prädikatenlogik zweiter Stufe gibt es wahre Aussagen, die kein Beweiskalkül ableiten kann.
Schritte zur Kojuktiver Normalform (KNF)
