Aufgabe:
Gibt es einen Trick beim Vorgehen bei Resolution (Aussagenlogik)?
Problem/Ansatz:
Ich hatte beispielsweise eine Aufgabe, bei der ich die Unerfüllbarkeit von:
{{¬A, B, ¬C}, {A, ¬C}, {¬A, C}, {B, C}, {A, ¬B}, {¬A, ¬B, ¬C}}
Zeigen soll.
Nach ewig langem rumprobieren kam ich dann auf den leeren Disjunktionsterm. Aber es muss doch irgendein System geben, wie man dabei vorgeht, sodass es keine Glückssache ist, ob die Aufgabe 1 Minute oder eine halbe Stunde dauert.
Danke
