Erfüllbarkeit und Entscheidbarkeit Flashcards
(28 cards)
Erfüllbarkeitsproblem - Definition
Allgemeingültigkeitsproblem - Definition
Problem der Semantischen Folgerung - Definition
Äquivalenzproblem - Definition
Auswertungsproblem - Definition
Reduzierung der algorithmischen Probleme in der Logik
Diese Probleme können alle auf nur zwei Probleme reduziert werden: Auswertungsproblem und Erfüllbarkeitsproblem
Auswertungsprobelm - Lösung
Das Auswertungsproblem der Aussagenlogik kann sehr leicht gelöst werden, z.B. durch einen einfachen rekursiven Algorithmus entsprechend der Definition der Semantikfunktion.
Erfüllbarkeitstest - Lösung
Verfahren zum Test auf (Un-)Erfüllbarkeit von AL - Formeln.
* Wahrheitstafeln
* Resolution
* Der DPLL Algorithmus
* Der aussagenlogische Sequenzenkalkül
* …..
Das Problem ist eines der am besten studierten Probleme der Informatik und ein NP-völlständiges Problem, es gibt jedoch Verfahren, die das Problem für viele in der Praxis vorkommende Formeln effizent lösen können
Kompaktheits- und Endlichkeitssatz - Definition
Theorem 3.4
Formel in KNF umwandeln
Klauselmenge - Definition
Klausel - Definition
Beziehung zwischen Klausel und KNF
Notationen für Formeln auf Klauselmengen
Erfüllung von Klauselmengen
Resolvente - Definition
Klauselmengen mit leeren Klauseln
Klauselmengen, die die leere Klausel enthalten, sind unerfüllbar
leere Klauselmengen
leere Klauselmengen sind immer Wahr/Allgemeingültig
Resolventen - Graphische Darstellung
Lemma - Resolvente von Klauselmenge mit Klauselmenge vereinigen
Resolutionsableitung - Definition
Resolutionswiederlegung - Definition
Resolutionswiederlegung - Beispiel
Korellation zwischen Resolutionswiederlegung und unerfüllbar
Eine Menge C von Klausen hat genau dann eine Resolutionswiderlegung, wenn C unerfüllbar ist.
