Ü2 H1a

kbraden
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 15. Okt 2010 20:35

Ü2 H1a

Beitrag von kbraden » 15. Jun 2011 20:11

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?

Matthias Senker
Windoof-User
Windoof-User
Beiträge: 41
Registriert: 14. Okt 2010 22:42

Re: Ü2 H1a

Beitrag von Matthias Senker » 15. Jun 2011 20:55

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.

kbraden
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 15. Okt 2010 20:35

Re: Ü2 H1a

Beitrag von kbraden » 15. Jun 2011 21:12

Okay, zwischenzeitlich (nach Begutachtung der Gruppenlösung) fiel mir auch auf dass das ja geht. Danke!

Antworten

Zurück zu „Archiv“