Resolutionskalkül

ez22
Mausschubser
Mausschubser
Beiträge: 71
Registriert: 28. Mär 2011 14:52

Resolutionskalkül

Beitrag von ez22 » 11. Aug 2011 11:09

hallo,

habe eine Frage zu dem Resolutionskalkül, und zwar geht darum ob man Klausel aus den ersten (davorigen) Resolventen doppelt benutzen kann?

z.B.:

Res0(K) = {{p, -q, r}, {-p, q, r}, {p, -q, -r}, {p, q} {-p}}
*weiter alle mögliche Resolventen werde ich nicht aufschreiben.

Danach folgen folgende Schritte:
1. {p, -q, r} und {p, q} => {p, r}
2. {p, -q, -r} und {p, q} => {p, -r} *hier wird die gleiche Klausel verwendet (doppelt)
3. {p, -r} und {p, r} = > {p}
4. {p} und {-p} = > 0 *hier wird die Klausel von dem ersten Resolventen verwendet

danke im Voraus!

Benutzeravatar
hymGo
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 209
Registriert: 4. Okt 2009 23:17

Re: Resolutionskalkül

Beitrag von hymGo » 11. Aug 2011 11:21

Zum Resolventen bilden steht dir alles was du schon abgeleitet hast zur Verfügung. Somit kannst du Resolventen auch doppelt benutzen.

Antworten

Zurück zu „Archiv“