http://3773.rapidforum.com/topic=101687299417kann eine klausel {A, nicht A} bei einer resolution ignoriert werden?
ja
ist eine klauselmenge, die {A, nicht B} und {B, nicht A} enthält,
immer unerfüllbar?
Nein A=1, B=1 oder A=0, B=0
wenn in einer klauselmenge die atomare formel A immer nur in der
form "nicht A" vorkommt, können dann die klauseln, die diese
"nicht A" enthalten, ignoriert werden?
Wenn A=0 gesetzt wird werden alle Klauseln mit nA wahr —> Klauseln können ignoriert werden
Würden solche Antworten auf die Fragen hinhauen?
so würd ich das auch beantworten..
Es geht hier doch um Resolution, oder? Dann waere eine Antwort, dass die Klauseln, die neg A enthalten stets (bei jeder Resolventenbildung) dieses neg A mit einbringen, was man nicht "wegkriegt" (da es kein Klausel gibt, die A enthaelt und mit der man resolvieren koennte). Die Klauseln die neg A enthalten koennen also in keiner Resolutionsableitung der leeren Klausel enthalten sein. D.h. andersherum wenn es eine Resolution zur leeren Klausel gibt, so wird dort nirgendwo mit einer Klausel die neg A enthaelt resolviert werden.
Hoff' es hilft [img]
http://www.fb18.de/gfx/28.gif[/img]
Cheers,
Frank
Jo, der Witz bei der Sache ist doch aber, dass alle Klauseln die das nA enthalten sowieso egal sind für die Resolution, da diese Klauseln immer wahr werden können. Deshalb ist es doch wichtig sich die anderen Klauseln anzugucken, ob dort die leere Menge resolviert werden kann, denn das würde ja bedeuten, dass mindestens eine Klausel ohne das nA nicht erfüllbar wäre —-> Formel nicht erfüllbar
(wenn ich das jetzt richtig interpretiere)
Es kann aber auch sein dass der Schädel schon zu stark raucht
Edit: Hmmm kann es sein, dass du genau das gesagt was ich gerade geschrieben hab? Ich raff nicht mehr soviel irgendwie
ja eigentlich schreibt ihr das gleiche [img]
http://www.fb18.de/gfx/24.gif[/img]
Ich hab echt genug mittlerweile, seit 3 Tagen immer 6 Stunden am Stück und davor auch schon gelernt, aber es ist so derbe viel.
Man findet immer wieder irgendwas was man noch nicht draufhat usw.
Frust pur….
Hm und wo liegt nun der Unterschied zwischen Grundresolution und prädikatenlogischer Resolution?
dass man bei der prädikatenlogischen subst auch in den prädikaten herumpfuschen (äh herumsubstituieren) darf *g*
dass man bei der prädikatenlogischen subst auch in den prädikaten herumpfuschen (äh herumsubstituieren) darf *g*
Also eine "Grundresolution" als solche gibt es nicht. Es gibt den Grundresolutionsalgorithmus, Grundsubstitutionen und prädikatenlogische Resolution allgemein.
Eine Grundsubstitution ist eine Substition, die alle Variablen durch variablenfreie Terme ersetzt (d.h. das Ergebnis ist in E(F)). Das Ergebnis wird dann auch Grundinstanz der Matrix genannt (zur Unterscheidung von allgemeinen Instanzen, das sind Substitutionsergebnisse, die evtl. noch Variablen enthalten).
Der Grundresolutionsalgorithmus ist ein Resolutionsverfahren, das ausschließlich Grundsubstition anwendet.
Allgemein darf man bei prädikatenlogischer Resolution auch Substitutionen vornehmen, sodass im Ergebnis noch Variablen vorkommen (man verschiebt dann quasi die restliche Grundsubstitution auf später).
