FB18.de - Das Informatikforum
Fragen zur Resolution aus Klausurabschrift - Druckversion

+- FB18.de - Das Informatikforum ( /mybb )
+-- Forum: Diplom Informatik ( /forumdisplay.php?fid=114 )
+--- Forum: Unterbereich Grundstudium ( /forumdisplay.php?fid=123 )
+---- Forum: Formale Informatik ( /forumdisplay.php?fid=16 )
+---- Thema: Fragen zur Resolution aus Klausurabschrift ( /showthread.php?tid=7401 )


Fragen zur Resolution aus Klausurabschrift - pRoMoE - 18.07.2004 17:12

http://www.fb18.de/rfmapper.php?mode=topic&tid=101687299417

kann 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?




Re: Fragen zur Resolution aus Klausurabschrift - Brokkoli - 18.07.2004 17:14

so würd ich das auch beantworten..


Re: Fragen zur Resolution aus Klausurabschrift - Azure - 18.07.2004 17:18

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

Cheers,
Frank


Re: Fragen zur Resolution aus Klausurabschrift - pRoMoE - 18.07.2004 17:26

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




Re: Fragen zur Resolution aus Klausurabschrift - Brokkoli - 18.07.2004 17:42

ja eigentlich schreibt ihr das gleiche


Re: Fragen zur Resolution aus Klausurabschrift - pRoMoE - 18.07.2004 18:20

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?


Re: Fragen zur Resolution aus Klausurabschrift - Brokkoli - 18.07.2004 18:30

dass man bei der prädikatenlogischen subst auch in den prädikaten herumpfuschen (äh herumsubstituieren) darf *g*


Re: Fragen zur Resolution aus Klausurabschrift - georg - 18.07.2004 21:42

Zitat:
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).