Eine aussagenlogische Formel ist erfüllbar genau dann, wenn
es eine Wertebelegung für die Aussagenvariablen gibt, die die Formel wahr macht.
Eine aussagenlogische Formel ist allgemeingültig genau dann, wenn
alle Wertebelegungen für die Aussagenvariablen die Formel wahr machen.
H |= G
Für (alle) A:N -> {0,1} (gilt :) mit A(P) = … ist A(H) = 1 und A(G) = 0
Eine Formel ist eine Horn Formel genau dann, wenn
wenn sie in KNF ist und pro Klausel maximal ein positives Lateral vorkommt
Horn-Formel nein erfüllbar
Nach Anwendung des Markierungsalgorithmus ist zu sehen, dass in Klausel (_) … _ und _ markiert sind. Also ist F unerfüllbar.
Horn Formel ja erfüllbar
Da es keine Implikation gibt, bei der die linke Seite vollständig markiert ist und die rechte Seite leer ist daher ist F erfüllbar.
Modell A:{…} -> {0,1} mit A(R) = A(.. = 1, A(.. = 0
Markierte Atome wahr; nicht markierte Atome falsch
Resolutionskalkül nein erfüllbar
Der Resolutionskalkül ist korrekt und es konnte die leere Klausel hergeleitet werden.
Tableaukalkül nein erfüllbar
Der Tableukalkül ist korrekt und es wurde ein geschlossenes Tableu gebildet
Tableaukalkül ja erfüllbar
Da wir ein voll expandiertes Tableau herleiten konnten, das nicht geschlossen ist, und der Tableaukalkül vollständig ist, ist die Klauselmenge erfüllbar.
MM unifizierbar ja
Es wurde nicht (Falsum) hergeleitet und es sind keine weiteren Schritte möglich
Unifikator: [Funktionssymbole/Variable …]
MM unifizierbar nein
Es wurde (Falsum) hergeleitet; .. und .. sind nicht unifizierbar.
Faktorisierungsregel
Resolutionsregel
Nicht faktorisierbar
Nicht faktorisierbar, da man (Variable) und (Funktionssymbol) unifizieren müsste, was nicht möglich ist.
Tableaukalkül Prädikatenlogik
Der Tableukalkül ist korrekt und es konnte ein geschlossenes Tableau hergeleitet werden.
Schließen aller offenen Äste mit dem mgu.. = [(Variable)/(Funktionssymbol)]
Zuletzt geändertvor einem Monat
