Resolutionskalkül / Klauselmenge



  • hi peoples

    hab grad in der uni in mathe das resolutionskalkül im zusammenhang mit klauselmengen gehabt und dazu hab ich ne frage

    Ich hab folgende Aussagenlogische Formel in KNF:

    [e]alpha[/e] = (a + b + c) ° (a + -b+ -c)
    

    (plus sei hier das logische ODER, und das zwischen den klammern soll UND heissen, und das minus vor den variablen ist das logische NICHT)

    so, dann sei

    M[t][e]alpha[/e][/t] = {(a, b, c), (a, -b, -c)}  [ = R[h]0[/h](M[t][e]alpha[/e][/t])
    

    so wenn ich jetzt das ganze Zusammenfasse müsste doch folgendes rauskommen:

    R[h]1[/h](M[t][e]alpha[/e][/t]) = {(a, b, c), (a, -b, -c),  (a, b, -b)}
    

    c und NOT c lassen sich ja gegenseitig auflösen, und b und NOT b bleibt übrig weil man das ja nicht 2 mal gleichzeitig machen darf (wurde uns gesagt)

    aber da das ganze ja eine oder verknüfung ist, ist das doch eine tautologie ?!?

    a ODER b ODER NOT b -> a ODER 1 -> 1

    was mache ich dann?
    bzw ist das richtig was ich da mache?
    in unserm script steht nichts zu dem fall und nen prof zu fragen hatte ich noch nicht die gelegenheit

    mfg zusammen



  • Ich schätze, das ist richtig. Du bekommst dann halt einmal $$\top$$ in deine Klauselmenge. Könntest du aber auch genausogut weglassen, weil du damit nicht weiter resolvieren kannst.



  • dieses T heist tautologie ?

    d.h. ich könnte diese klausel eifnach rausstreichen?

    hab nämlich in ner aufgabe damit sauviele neue klauseln erstellt bis ichd ann irgendwann keine lust mehr hatte und aufgehört hab



  • Ach sorry, das hab ich vergessen zu schreiben. Dieses Symbol steht für "wahr" (vielleicht weil es wie das T von true aussieht). Umgekehrt steht $$\bot$$ für "falsch".

    Ja, man kann die Klausel dann auch streichen. Da du weiter nichts machen kannst, ist das Verfahren damit beendet.


Log in to reply