Hallo zusammen

kann mir mal jemand einen Tipp geben, wie man anzufangen hat?
Die Aufgabe ist es die Resolutionsregel {(A v B), -A v C)} |- (B v C) als geltend zu zeigen, mit hilfe von dem Axiom ((-A -> -B) -> (B -> A))
Außerdem kann man noch Modus Ponens und die abgeleitete Inferenzregel Transition benutzen. Nun sitze ich hier und frage mich, WIE fängt man an? Wenn ich es richtig verstanden habe, ist das ziel, am Ende die Resolutionsregel als B im Modus Ponens zu haben. Stimmt das? Womit fängt man dann an?

Vielen Dank und einen guten Rutsch.

tja, Tipp..,

schau mal die Transitionsregel an,

wenn du da alle Variablen geeignet umbenennst und A3 sowie die beiden Definitionen anwendest,
kommt irgendwann die Resolutionsregel raus

zu a)
Bin mir nicht ganz sicher ob ich das jetzt richtig verstanden habe. Also ist folgendes mit hilfe des Modus Ponens zu zeigen:
((A+B)* (-A+B)) -> B+C !?

im Grunde ja,
genauer: {(A v B), -A v C)} |- (B v C)
das ist eventuell der Definition nach was leicht anderes?

Ich fände es toll, wenn ihr oder sonst jemand vielleicht mal den ersten Schritt machen könnte?! Oder mir sonst irgendwie einen weitergehenden Tipp geben könnte. Ich sehe einfach nicht, womit ich anzufangen habe.
Also ich meine, wie ich substituiere um zu irgendwas zu kommen was ich gebrauchen kann.

Beispiel:
z.Z.: (A v B) -> (B v A)

A v B = -A -> B (Def.)

(-A -> B) -> (-B -> A) (A3)

-B -> A = B v A (Def.)

also folgt (A v B) -> (B v A)

kann sein, dass ich die Aufgabe zu einfach sehe,
aber mit solch simplen Umformungen scheint das ganze zu funktionieren

Danke für das Beispiel.
Ich verstehe das Prinzip. Ich weiß einfach nicht, womit ich anfange. Sehe das einfach nicht, denke ich werde einfach mal abwarten und gucken ob die Lösung mir die Erleuchtung bringt.

Trotzdem Danke nochmal!