Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Frage zu Resolution
Mal angenommen ich würde folgende Formel mit Tableaux oder Resolution lösen auf Gültigkeit überprüfen wollen
Dann müsste ich ja quasi z.B. bei Resolution Definition 2.1 auf Slides F461 anwenden. Die Regel für Tableaux ist ja fast identisch.
.
In dem Fall wären allerdings keine freien Variablen in der Formel vefügbar die mit f_n^k(X^1 ,…, X^k) substitutiert werden hätten können? Wie geht man hier dann vor?
Dann ist f 0-stellig, also ein konstantensymbol 
Wenn ich diese Aufgabe mit Resolution weiterrechne dann lande ich irgendwann bei folgender Zeile:
Resolution terminiert dann wenn zwei Klauseln sich (edit:) gänzlich zur leeren Klausel “wegküzen” wie hier mit dem R ganz links und dem R ganz rechts. Es müssen sich nicht alle Klauseln weghebeln oder? Das hat den Hintergrund, dass man gezeigt hat das wie hier die linke Klausel und die ganz rechte Klausel nicht gleichzeitig True und False sein können oder? In den Beispielen wie z.B. Slides F362 oder Problem 10.2 in den Assignments haben sich immer alle Klauseln weghebeln lassen.
Beim Tableux habe ich gesehen, dass man aufhören kann sobalt ein Konflikt vorliegt.
Wooah, wenn du das so notierst zieh ich in der Klausur Punkte ab 
Nee, im ernst, lass doch die leeren Klammern weg, die sind unnötig und machen alles schwerer zu lesen 
Ansonsten hast du recht, resolution terminiert genau dann wenn du eine(!) leere Klausel erzeugen kannst 