formelmenge:
{D=>(AvAvC),(C^D)=>(AvB),D,not((AvB)^D)}
klauselform:
{notD,A,B,C} {notC,notD,A,B} {D} {notA,notB,notD}
dann mit linearer resolution auf erfüllbarkeit prüfen.
da bekomme ich dann die klausel {notD} raus
stimmt das so oder mache ich was falsch?
ich hab irgendwie die leere Menge raus…..also ist die Formel unerfüllbar oder????
ich habe irgendwo einen fehler, weiss nich wo, kann mal jemand die richtige klauselmenge angeben bitte?
{notA,notB,notD}
Ist die Klausel hier nicht falsch?
Wenn man "not((AvB)^D)" hat, wird das mit de Morgan doch "(notA ^ notB) v notD".
Das ist zwar keine Klausel, aber ich wüsste nicht, wie man die umformen soll, so dass das obige herauskommt.
{notA,notB,notD}
Ist die Klausel hier nicht falsch?
Wenn man "not((AvB)^D)" hat, wird das mit de Morgan doch "(notA ^ notB) v notD".
Das ist zwar keine Klausel, aber ich wüsste nicht, wie man die umformen soll, so dass das obige herauskommt.
wie bringe ich das dann in klauselform?
genau das ist grad mein problem
aus "(notA ^ notB) v notD" kann man doch wegen der Distributivität "(notA v notD) ^ (notB v notD)" machen
oh, danke! auf sowas naheliegendes komme ich natürlich wieder mal nicht.
und ist die formel nun erfüllbar oder nicht….kriege eine leere menge raus…also unerfüllbar.
ich bekomme am ende immernoch {notD} herraus. was mache ich falsch???
ich bekomme am ende immernoch {notD} herraus. was mache ich falsch???
oh, neheme ich dann das notD mit dem D und bekomme die leere klausel? aber ist das dann noch linear?…