ich schreibe meine formel in implikationsschreibweise um…

dann habe ich die teilformel …. and(AandC)=>bottom

wie behandle ich diesen fall bei der makierung?. im skript gab es kein beispiel, in dem eine hornklausel mit nur negativen literalen vorkommt

Dann schau Dir mal Folien 13/14 in Kap. 7 an - da stehts doch ganz eindeutig.

Am besten ich erkläre nochmal den gesamten Markieralgorithmus (aber nicht formal ;-)):

1. Forme Hornformel in implikativer Schreibweise um.
2. Markiere alle atomaren Formeln A für die gilt: Top => A
(also wenn man eine Formel (Top => A) hat, dann markiere überall das A)
Begründung Top ist Tautologie und die TeilFormel (Top => A) kann nur wahr werden wenn
A nicht falsch ist. Durch die Markierung merken wir uns sozusagen, dass "A = 1" gelten muss.

3. Nun kann es nur noch zwei Arten von Teilformeln geben:
1 (A1 and A2 and … and An) => B (B ist atomar) n >=1
2 (A1 and A2 and … and An) => Bottom n>=1

Solange es solche Teilformeln gibt , ! wobei A1 bis An schon markiert ist ! führe dies durch:
(wenn es keine von disen Teilformeln gibt, dann ist die Formel erfüllbar)

Wenn eine Teilformel den Fall 1 entspricht markiere jedes vorkommen von B (B siehe 1)
Begründung: Bsp: man habe die Teilformel (A and B) => C , wobei A und B jeweils schon
markiert sind. Dann wissen wir A und B müssen den Wahrheitswert 1 haben
Also muss ,damit (A and B ) => C wahr wird, C auch markiert werden und somit den
Wahrheitswert 1 zugeteilt bekommen.

Wenn eine Teilformel den Fall 2 entspricht dann ist die Formel unerfüllbar.
(Begründuing: Bsp: man habe die Teilformel (A and B) => Bottom wobei A und B markiert
sind, also wir haben schon vorher gemerkt, dass jeweils A und B wahr sein müssen.
daher kann dann (A and B ) => Bottom nicht wahr sein.
denn 1 => 0 (nicht formal) geht nicht.


Nun zu deinem Fall : (A and B) => bottom
Es kommt auf deine Markierung von A , B an:
Sind A und B jeweils beide markiert ist die Formel unerfüllbar.
Ist nur eine von den beiden markiert brauchen wir uns um diese
Formel vorerst oder auch gar nicht kümmern.

Bsp wäre
F sei :( ( A and B ) => bottom ) and ( Top => A)

Schritt 1. Formel ist bereits in implikativer Schreibweise
Schritt 2. markiere A
( ( A' and B ) => bottom ) and Top => A'
Schritt 3. Es gibt keine Teilformel wobei A1 and … and An bereits markiert sind
=> Formel ist erfüllbar.


erfüllende Belegung für F : A = 1 und B = 0
(Alle markierten atomaren Formeln erhalten den Wahrheitswert 1, die unmarkierten 0)

ich bekomme bei der ersten formel erfüllbar raus… aber mit nur einer möglichen belegung. ist das richtig?

aber wenn es nur eine solche belegung gibt dann ist sie ja nicht minimal, wenns eh nur eine gibt… deswegen frage ich mich ob meine lösung richtig ist.

wenn jemand mehrere belegungen raus hat, welche habt ihr dann? vieleicht sehe ich dann was ich falsch mache, wenn ich es denn falsch mache….

mit dem markierungsalgorithmus bekommst du eine mögliche belegung heraus, es kann noch mehr geben.

wenn a und c bei ((a ^ c) => bottom) markiert sind, tritt im zweiten schritt des algorithmus der else fall ein und die formel ist nicht erfüllbar.

meine frage war direkt zu der ersten formel in der aufgabe, wo ich nur eine mögliche erfüllende belegung bekomme. ich weiss es kann mehrere geben, und dann spricht man von minimaler belegung.

meine frage nun, gibt es zu der ersten formel in aufgabe 7.1. mehrere erfüllende belegungen?

b könnte zum beispiel auch 1 sein.