Resolutionskalkül: Beweis

Question

ich soll zeigen, dass:

R_i ⊆ Resⁱ(K(F)

gilt.

Also dass die i-te Menge der Resolutionsklauseln eine Teilmenge der Resolutionsmenge von der Klauselmenge von F ist.

Ist das nicht beides das gleiche? Wie beweise ich das am besten?

Danke und Grüße!

Comments

Bitte erläutere noch mal, was R_i sein soll, am besten durch die wörtliche Definition, die ihr verwendet habt.

---

Hallo oswald,

danke für deine Antwort. Im Anhang ist der Teil, wo Ri  vorkommt.

Nach meinem Verständnis ist das die Menge der Klauseln von Resⁱ(K(F)), oder?

Answer 1

Laut meiner Definition von Res_i(K(F)) wird Res_i(K(F)) aus Res_i-1(K(F)) gebildet indem die Resolventen von jedem Klauselpaar aus Res_i-1(K(F)) hinzugefügt werden.

Laut deiner Definition von R_i wird R_i aus R_i-1 gebildet, indem die Resolvente von einem Klauselpaar aus R_i-1 hinzugefügt wird.

Damit sollte die genannte Teilmengenbeziehung offensichtlich sein. Beweis geht mit vollständiger Induktion.

Comments

Ahh ok danke, da liegt also der Clue.

Ich habe damit angefangen, aber komme nicht so wirklich weiter... kannst du mir vielleicht noch einen Tipp geben?

Beweis durch Induktion

Induktionsbehauptung:

R_i ⊆ Resⁱ(K(F)) mit R₀ = K(F)

Induktionsanfang:

Sei i = 1, dann

        R₁ ⊆ Res¹ (K(F))

<=>  K(F) ∪ X ⊆ Res¹(K(F))

In der Resolventen von K(F) sind alle Klauseln von K(F) sowie ihre zugehörigen Resolutionen enthalten. Da X eine dieser Resolutionen darstellt, und diese mit K(F) verbunden wird, muss R₁ eine Teilmenge von K(F) sein.

Induktionsvoraussetzung:

R_i ⊆ Resⁱ(K(F)) 

Induktionsschritt:

Sei i = i+1

       R_i+1 ⊆ Resⁱ⁺¹(K(F))

<=> R_i ∪ X ⊆ Res(Res¹(K(F)))

Hier stockts jetzt..

---

Als Induktionsanfang würde ich i=0 nehmen: es ist R₀ = K(F) und Res⁰(K(F)) = K(F). Wegen K(F) ⊆ K(F) ist also R₀ ⊆ Res⁰(K(F)).

Für den Induktionsschritt sei 0 < n ∈ ℕ und für jedes i < n gelte R_i ⊆ Resⁱ(K(F)). Ferner sei K eine Klausel aus R_n.

Fall 1: K ∈ R_n-1. Wegen R_n-1 ⊆ Res^n-1(K(F)) ist dann K ∈ Res^n-1(K(F)). Wegen Res^n-1(K(F)) ⊆ Resⁿ(K(F)) ist dann auch K ∈ Resⁿ(K(F)).

Fall 2: K ∉ R_n-1. Seien dann K₁, K₂ zwei Klauseln aus R_n-1, so dass K Resolvente von K₁, K₂ ist (solche Klauseln existieren aufgrund der Definition von R_n). Wegen R_n-1 ⊆ Res^n-1(K(F)) sind dann K₁ und K₂ auch in Res^n-1(K(F)) enthalten. Aufgrund der Definition von Resⁿ(K(F)) ist dann auch K ∈ Resⁿ(K(F)).

> Sei i = i+1

Es gibt kein i, dass diese Bedingung erfüllt.