Seite 1 von 1

Ü2 H1a

Verfasst: 15. Jun 2011 20:11
von kbraden
Wenn ich den Resolutionsalgorithmus auf die Klauselmenge die aus der gegebenen Formel entsteht, anwende, komme ich auf über 50 Klauseln nach Res2(K), bevor ich mit Res3(K) die leere Klausel ableiten kann. Soll das so sein oder mach ich was falsch?

Re: Ü2 H1a

Verfasst: 15. Jun 2011 20:55
von Matthias Senker
Also ich würde mal sagen, dass es ausreicht, die Ableitungen zu bilden, die man auch braucht. :wink:
Im Skript steht, dass ein Beweis im Resolutionskalkül ein Baum ist, mit den Anfangs-Klauseln in den Blättern und der leeren Klausel in der Wurzel. Daran würde ich mich bei dieser Aufgabe orientieren.
Es geht sicher nicht darum blind alle Ableitungen hinzuschreiben, sondern darum, am Ende einen korrekten Beweis zu haben.

Re: Ü2 H1a

Verfasst: 15. Jun 2011 21:12
von kbraden
Okay, zwischenzeitlich (nach Begutachtung der Gruppenlösung) fiel mir auch auf dass das ja geht. Danke!