Date of registration: Dec 11th 2001
Location: Hämelerwald
Occupation: Wissenschaftlicher Mitarbeiter (Forschungszentrum L3S, TU Braunschweig)
Monday, May 2nd 2005, 9:41am
Beides ist möglich.
Quoted
Original von snoopy
Ich habe in der Klauselmenge die Klauseln {nA, C} und {A, B, nC}
Ich weiß nicht, was ich genau daraus resolviere, wenn nun mehere "Paare" in 2 Klauseln sind. Was wird daraus?
1) {B}
2) {B, C, nC} und {A, nA, B}
Ja und ja.
genauso ratlos bin ich in einem Fall wie {A,B} und {nA, nB}. Kann ich da in EINEM Schritt die leere Klausel resolvieren? Gebe ich diese eigenltlich mit in Res^x mit an?
This post has been edited 1 times, last edit by "Joachim" (May 2nd 2005, 9:42am)
Monday, May 2nd 2005, 4:30pm
Ja und ja.
genauso ratlos bin ich in einem Fall wie {A,B} und {nA, nB}. Kann ich da in EINEM Schritt die leere Klausel resolvieren? Gebe ich diese eigenltlich mit in Res^x mit an?
Zumindest die Definition im Buch von Schöning (Seite 38/39) läßt auch mehrschrittige Resolution zu, und ich nehme an, daß Herr Steffens das genauso sieht. (Schau Dir mal seine Definition aus der Vorlesung an.)
This post has been edited 2 times, last edit by "DrChaotica" (May 2nd 2005, 5:54pm)
Date of registration: Dec 11th 2001
Location: Hämelerwald
Occupation: Wissenschaftlicher Mitarbeiter (Forschungszentrum L3S, TU Braunschweig)
Monday, May 2nd 2005, 6:00pm
Du hast natürlich recht. Ich hätte die Defintion genauer lesen sollen.
Original von DrChaotica
Ja und ja.
genauso ratlos bin ich in einem Fall wie {A,B} und {nA, nB}. Kann ich da in EINEM Schritt die leere Klausel resolvieren? Gebe ich diese eigenltlich mit in Res^x mit an?
Zumindest die Definition im Buch von Schöning (Seite 38/39) läßt auch mehrschrittige Resolution zu, und ich nehme an, daß Herr Steffens das genauso sieht. (Schau Dir mal seine Definition aus der Vorlesung an.)
Interessant.
In unserer Vorlesung haben wir gehört: "Eine Klauselmenge, welche die leere Klausel enthält, wird als unerfüllbar bezeichnet".
{A, B, C}. ({A, B} aus der ersten Klausel und {B, C} aus der zweiten).
EDIT: Noch eine interessante Frage in diesem Zusammenhang: Was liefert {A, nA, B} und {A, B, C}? Etwa {A, B, C}, oder, wie ich denke, {B, C} ...
Monday, May 2nd 2005, 6:25pm
Original von snoopy
Ich habe mal eine Frage zur Resolution.
Ich habe in der Klauselmenge die Klauseln {nA, C} und {A, B, nC}
Ich weiß nicht, was ich genau daraus resolviere, wenn nun mehere "Paare" in 2 Klauseln sind. Was wird daraus?
1) {B}
2) {B, C, nC} und {A, nA, B}
genauso ratlos bin ich in einem Fall wie {A,B} und {nA, nB}. Kann ich da in EINEM Schritt die leere Klausel resolvieren? Gebe ich diese eigenltlich mit in Res^x mit an?
This post has been edited 1 times, last edit by "Markus" (May 2nd 2005, 6:29pm)
Date of registration: Dec 11th 2001
Location: Hämelerwald
Occupation: Wissenschaftlicher Mitarbeiter (Forschungszentrum L3S, TU Braunschweig)
Monday, May 2nd 2005, 6:32pm
Durch Resolution von { {A, B, C}, {!A, !B, C} } erhält man { {A, B, C}, {!A, !B, C}, {B, !B, C}, {A, !A, C} }.
Original von Markus
Mit einem ähnlichen Problem habe ich heute Herrn Steffens nach der Vorlesung angesprochen.
{A,B,C},{nA,nB,C}
Er meinte, {C} sei an dieser Stelle falsch, es müsse {B,nB,C} heißen, sowie {B,nB,C}.
Allerdings meinte er auch, dass {B,nB} ja nichts weiter als 1 sei.
Also hat man dann doch {C}. ?!
This post has been edited 2 times, last edit by "Joachim" (May 2nd 2005, 6:40pm)
Monday, May 2nd 2005, 6:37pm
Original von Joachim
Du hast natürlich recht. Ich hätte die Definition genauer lesen sollen.
Die Resolution erfolgt immer nur für genau ein Literalpaar.
Sunday, July 16th 2006, 4:18pm
Original von Neo
In der Musterlösung steht folgendes für (k1, kj): (j >= 7)
{A, !B, C}, {A,C}, {!A, A}, {!B, B}, {!B, C}
Kann es sein, dass es sich bei {!A, A} um einen Druckfehler handelt?
Ich kann mir leider nicht erklären, wie man diese Klausel resolviert.
Weiß jemand weiter?
