Bei a habe ich folgendes gemacht..
Ansatz phi |= psi
dann die Allquantoren entfernt
Pet(c) -> Cat(c) v Dog(c) & Cat(c) -> Cute(c)
dann die Wahrheitstabelle gemacht und überprüft ob jede Belegung die phi 1 werden lässt auch psi 1 werden lässt..
bei b) habe ich beide Formeln in NNF gebracht und den Ansatz
phi |= psi iff phi & -phsi is unsatisfiable..
dann habe ich den Baum gemacht und in jedem branch kam ein clash vor.. also
gilt phi |= psi
kann das stimmen?
Last edited by Turbosailor; 07-04-2012 at 11:37.
Das bei a) mit der Wahrheitstabelle wuerd ich nicht so machen. Machs wie in Bsp 1)
Ich habe den selben Ansatz für b verfolgt, jedoch komme ich dabei auf sehr viele Branches und das ganze wird bei mir irgendwie satisfiable. :/
Ich habe a -> b mit -a v b ersetzt, phi ist die KB und psi ist der Query.
Last edited by Jukebox; 11-04-2012 at 18:30.
The floor is now lava.
du musst -a & b nehmen.. nicht v
Was meinst du mit a und b? Wenn du nur in nnf transformierst, dann passt das oder schon.
phi |= psi iff phi & -phsi is unsatisfiable..
Wenn er aber bereits das erkannt hat und nur a->b transformiert, dann muss er es aequivalenzerhaltend machen. |= ist konzeptionell was anderes wie ->
ist bei dir das entailment gültig oder nicht?
Ja, ist gueltig. Kann eh sein, dass er genau das falsch machst was du meinst. Soweit ich das verstanden hab, will er nur in nff transformieren
hat sich für mich so angehört, dass er das eintailment meintOriginally Posted by Jukebox
also ist eh alles in ordnung
Jetzt habt ihr mich verwirrt.
Das Entailment hab ich mit a ^ -b ersetzt, ja.
-> hab ich mit -a v b ersetzt.
Das Problem ist folgendes: Ich habe die NNFs gebildet und dann per TC versucht zu beweisen dass a ^ -b unsatisfiable ist (wobei a die KB und b der Query ist). Ich komme jedoch auf Branches die keine Clashes enthalten. Es werden auch sehr viele Branches.. so in etwa 18, deswegen vermute ich eben dass ich irgendetwas vertauscht habe, aber ich komme immer auf das selbe Ergebnis.
The floor is now lava.
18 branches sind zu viel. Verwendest du die Inferenzregeln richtig? Richtige nff? Mehr kann ich von hier aus mit der bekannten information nicht sagen.
Ah, ich habe vergessen De-Morgan auf die Negation des Queries anzuwenden!
Jetzt clasht es überall.
Last edited by Jukebox; 11-04-2012 at 18:44.
The floor is now lava.
warum nicht? wenn ich's wie bsp 1 mache, dann ist das mehr oder weniger TC ohne dass ich es wie TC anschreibe ;-)
Wohl oder uebel macht ein Kalkuel nichts anderes, als dass er aehnlich verfaehrt wie "using semantics". Wahrheitstabellen werden dir aber bei der Formel von Bsp 5 trotzdem nix bringen
Nichts bringen im Sinne von nicht akzeptierter Lösungsweg? Weil funktionieren tuts ja!Wohl oder uebel macht ein Kalkuel nichts anderes, als dass er aehnlich verfaehrt wie "using semantics". Wahrheitstabellen werden dir aber bei der Formel von Bsp 5 trotzdem nix bringen
Wuerdest du jede Praedikatenlogische Formel mit Wahrheitstafel entscheiden koennen, dann waer das Gueltigkeitsproblem nicht semientscheidbar. Also nein, das wird kein akzeptierter Weg sein.
Wie sieht den eure NNF aus von der ihr dann den Baum aufbaut?
Ich befürchte, dass ich da was falsch habe und deshalb nicht wirklich weiterkomme. Ich hab insg. 4 ^, 4 v, 4 not
Wie leite ich den Baum her, wenn ich die Form (avb) & (bvc) & (cvd) habe? Die drei Klammern untereinander und dann davon ausgehend 6 einzelne Zweige weg? :\
schau, dass du die & zwischen den klammern eliminierst, indem du auswertest:
(avb)&c wird zu a&c v b&c... somit muss entweder ersteres oder letzteres gelten (dass sind deine zweige)
genauso machst du's auch für deine formel. ist etw. länger, aber das prinzip ist dasselbe
Zu a), ich will doch zeigen dass phi ^ !psi unsatisfiable ist.
Ist es dann ein gültiger Weg ein Modell für Psi anzunehmen bei dem dieses 0 ergibt, und dann dieses Modell für Phi anzuwenden (und zu zeigen dass dieses 1 wird)? Oder muss ich immer zuerst vom Modell für Phi ausgehen?
Ich hab mir gedacht es ist einfacher wenn ich von Psi ausgehe, aber wenn ich das Modell von Psi hernehme, wie weiß ich dann ob c ein Element der Interpretation I(Cat) ist, das kommt da ja nicht vor? Darf ich das beliebig annehmen?
Blöde Frage. Damals in TIL haben wir angenommen, dass unsere Formel nach false evaluiert, und falls man das Tableau schließen, also in jedem Zweig einen Clash erzeugen kann, stimmt das nicht und wir wissen, dass die Formel immer true ergibt, ansonsten waren halt die Gegenbeispiele ablesbar.
Mit NNF haben wir die Tableaux auch nicht gefüttert, und die Ableitungsregeln waren dann halt abhängig davon, welchen Wahrheitswert die Teilformel annehmen muss.
Hier ist das Vorgehen anders, denn wir nehmen keinen Wahrheitswert an, somit sind auch die Ableitungsregeln nicht an diese gekoppelt. Wäre es falsch, wenn ich diese Aufgabe so löse, wie wir es in TIL gemacht haben? Warum unterscheiden sich die Vorgehensweisen?
Nachtrag: Ich seh grad, beim zweiten Beispiel in den Folien wird es doch so gemacht. Was ist denn jetzt genau der Unterschied? Ich hatte es nämlich bei TIL so verstanden, dass man bei diesem Kalkül generell über die Annahme des Gegenteils geht.
Last edited by ri_ba; 12-04-2012 at 21:34.
Dank dem Tipp bin ich jetzt tatsächlich auf 6 Zweige gekommen, von denen jeder clasht. Ich schätze, damit ist das Beispiel erledigt.
Eine Frage hab ich aber trotzdem noch: Warum wird a |= b zu a ^!b ?
Meine bisherige Erklärung wäre ja, dass 1 |= 0 ungültig wäre und man versucht, das zu zeigen, daher a ^!b. Allerdings hab ich mir diese Erklärung mangels Alternativen selber an den Haaren herbeigezogen. In den Folien habe ich dazu nix gefunden. Bei der "normalen" Variante (zB. 5a) macht man das nicht, da man nach dem Deduktionstheorem ja einsetzen kann, sodass a -> b zu 1 -> 0 wird. Seh ich das richtig? Ich bezweifle es
a |= b wird zu a ^!b, weil a |= b genau dann gilt, wenn a ^!b unsat ist.
Last edited by _gerald_; 15-04-2012 at 13:23.
also irgendwie stell ich mich beim Baum grad dumm an, k.A. wo es da hapert. Ich hab jetzt mal meinen aktuellen Stand drangehängt, vielleicht kann mir jemand sagen, ob das bis hierher mal soweit passt. Und falls ja, ob ich jetzt dann auch das letzte UND noch ausmultiplizieren soll, was dann zu einer ewig langen Formel führen würde, in der dann auch schon öfter unmögliche Teile vorkommen, wie P und Nicht P zum Beispiel.
ich bin mit
und
ins tableau eingestiegen, und hab 4 geschlossene branches. sonst noch jemand?
Ich komme auch auf 4 branches. Die 2 Allquantoren könnte man noch zu einem Allquantor zusammenfassen.ich bin mit
und
ins tableau eingestiegen, und hab 4 geschlossene branches. sonst noch jemand?
hab auch 4 branches, alle clashen; jedoch habe ich phi & nicht psi in NFF transformiert und dann abgeleitet.
heißt das, du bist mit einer Implikation ins Tableau eingestiegen? Ich dachte, das Tableau muss in NNF sein, und dann darf ja keine Implikation mehr drin sein, oder hast du das danach noch gemacht?ich bin mit
und
ins tableau eingestiegen, und hab 4 geschlossene branches. sonst noch jemand?
Ich hab mich auf die Folie "Reduction to stisfiability" bezogen, in der steht:
und das hab ich auf die KB und die Query angewandt, aber irgendwie häng ich da grad.
Das mit der nff passt scho. Schau dass du zuerst alle Konjuktionsterme untereinanderschreibst (das macht man praktischerweise als erstes). Dann solltest du mit der Allquantor-Beseitigung und den Disjuktionen auf 4 Branches kommen.
also ich hab jetzt nach der Allqantoren-Beseitigung folgendes stehen:
und das wäre jetzt die NNF von Phi AND NOT Psi und somit mein Beginn. Heißt das, bis hierher passts mal?
Duerfte imho passen.
jo, es gibt Tableau Regeln für Implikationen (siehe TIL skriptum)
f: A -> B
wird zu
t: A
f: B
was mEn den beweis verständlicher macht
Aber nicht fuer _diesen_ Kalkuel in dieser VO. Kalkuel ist nicht gleich Kalkuel.
das versteh ich nicht, wie viele Semantische Tableau-Kalküle gibts?
Ein Kalkuel ist definiert durch seine Axiome und seine Inferenzregel. Du hast im TIL Skript auch Gentzenkalkuele oder einen Hilbert-Typ-Kalkuel. Deswegen darfst du auch nicht die Regeln untereinander tauschen. Klar gehts auch mit Implikation, aber imho wuerde es an der Tafel nicht "gut ankommen", wenn du die TIL-procedure verwendest und nicht die der VO
ok, danke mal fürs drüber schauen, das hilft schon mal weiter. Aber irgendwie bin ich mit dem Kalkül noch etwas auf Kriegsfuß, ich hab das jetzt mal so versucht wie angehängt, bin davon aber nicht recht überzeugt. Darf ich das, in der 5. Zeile bei dem ODER aufspalten, also einen der UND-verknüpften Ausdrücke, und dann wieder gerade nach unten um dann noch den längsten der UND-verknüpften Ausdrücke aus der Startformel einfach dranzuhängen?
das tafel argument seh ich ein. auf der anderen seite denk ich mir "it's fucking logic", die regeln sind (obwohl sie aus dem TIL skriptum kommen!!) fürs semantische tableau schlüssig und korrekt, wieso sollt ich's nicht verwenden "dürfen".
naja, schätz ich bau das halt so wie's in den folien "erwünscht ist". alles akademische faschisten auf der uni!
@testsieger: das was du da gezeichnet hast ist kein baum
@thrau: naja, das ist mal so. Wieso solltest keinen automatischen Beweiser verwenden "duerfen"?
weil die angabe sagt "check [by hand] using tableau calculus ..." (inhalt der klammern inferiert)@thrau: naja, das ist mal so. Wieso solltest keinen automatischen Beweiser verwenden "duerfen"?
aber nicht "check using tableau calculus BUT DO NOT USE VALID IMPLICATION RULES OR EGLY WILL EAT YOUR FACE"
whatevah!
Last edited by thrau; 15-04-2012 at 18:13.
stimmt natürlich, und die Klammerung hab ich auch übersehen, danke für deine Tipps. Leider fehlt mir da immer noch was, wie das Ding jetzt wirklich funktioniert. Ich hab jetzt also 3 durch UND verknüpfte Konnektoren, die schreib ich untereinander. Soll ich dann, wenn einer der neuen Teile aus mehreren Teilen besteht, diese gleich zerlegen? Ich häng da echt grad total, und irgendwie helfen mir die da Beispiele auf den Folien nicht weiter, die sind immer so eindeutig.@testsieger: das was du da gezeichnet hast ist kein baum
Jetzt schreibst du noch die restlichen Konjunktionsterme darueber und dann spaltest du einen Disjunktionsterm auf (fang mit dem einfachen, aus zwei atomen bestehenden an). Dann hast du gleich mal einen Clash.
sorry, ich muss leider noch mal nachfragen: was genau meinst mit die restlichen Konjunktionsterme drüber? Heißt das, ich zerlege z.B. zuerst den ganz rechten Konnektiv in Atome und mach dann mit restlichen Teil aus der ersten Zeile weiter?
genau, is einfacher bzw übersichtlicher so. und ob du rechts oder links als erstes machst, spielt denk ich keine große rolle sonst.
also bis hierher wie im angehängten Bild würde der Baum dann also mal passen, oder? Falls ja, ist mir aber dann erst recht noch immer nicht klar, wie ich dann weiter machen muss, weil ich da ja jetzt an einem Ende angekommen bin. Wie komm ich da zu den anderen Branches?
tut mir leid, das weiß ich leider nicht. das problem kannst du allerdings umgehen, indem du (a v b v c) ^ (d v e) einfach "ausmultiplizierst" zu (a ^ d) v (a ^ e) v (b ^ d) ...... usw. dadurch entstehen zwar mehr branches, allerdings fällt das problem weg, das mir auch zu schaffen macht. vllt kann uns der gerald da noch aufklären, oder einfach die übungsgruppenleiter ab morgen
@testsieger: Es hätte sich wohl angeboten, zuerst das linke ODER aufzubrechen. Du hast dann zwar drei Branches, aber zwei davon führen schon zu einem Widerspruch, und nunmehr in einer müsstest du dann das rechte ODER aufbrechen und dort deinen gewünschten Widerspruch kriegen.
Grafik
Last edited by Ravu al Hemio; 15-04-2012 at 21:44.
ich hab das heut mit egly nochmal abgeklärt: bei der klausur ist's ihm relativ egal was wir wie verwenden, die beispiele sind aber natürlich auf die behandelten methoden in der vorlesung zugeschnitten.Klar gehts auch mit Implikation, aber imho wuerde es an der Tafel nicht "gut ankommen", wenn du die TIL-procedure verwendest und nicht die der VO
was die übung angeht sollte man's wie auf den folien beschrieben machen.
ergo: i yield.
jedenfalls hab ich meine lösung mal ins vowi gestellt.
https://vowi.fsinf.at/wiki/TU_Wien:E...1_-_Beispiel_5
/add
ups, da is ja über mir schon was! naja, zumindest ists im wiki
@thrau gerade am Durchgehen meiner Übungsmitschriften, ohne deinen Vowi Eintrag hätte ich das nimmer gechecked - Danke
Es gibt nichts gutes, außer man tut es!
- Erich Kästner
Posting Permissions
Reply With Quote
Bookmarks