Teil A

1. Eliminieren Sie in folgender Formel den Pfeil -> und testen Sie die resultierende Formel zunächst per Hand mit dem markierten Tableaualgorithmus auf Allgemeingültigkeit. Nutzen Sie nun den Tableaubeweiser zum Test. Versuchen Sie den Beweis nachzuvollziehen und ihn mit Ihrer manuellen Ableitung abzugleichen; wo gibt es Gemeinsamkeiten, wo sind Unterschiede? Versuchen Sie den Algorithmus im Beweiser zu beschreiben, indem Sie u.a. das Konzept des aktuellen Zweigs, der möglichen Expansionen etc. einbeziehen.

   p v (q & r) -> (p v q) & (p v r)

2. Sehen sie bereits Stellen, an denen eine Optimierung ansetzen könnte?

Teil B

1. (s v h) v (q & r) -> ((s v h) v q) & ((s v h) v r)

   Was fällt im Vergleich zur Formel in Teil A) 1) auf? Konkret: Was beherrscht der TB noch nicht?

2. or - or p and q r and or p q or p s

   Wie lautet das falsifizierende Modell?

3. ((b<->c)->(a&b&c)) & ((c<->a)->(a&b&c)) & ((a<->b)->(a&b&c)) -> (a&b&c)

4. "Reihenfolge spielt eine Rolle"
   1. or or or or or or or or or or or or or or or or or or 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 - 1
   2. or or or or or or or or or or or or or or or or or or 18 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 1 - 1

5. Formalisieren Sie das Schubladenprinzip: Für jedes n (n eine natürliche Zahl) gilt: Versucht man n+1 Gegenstände auf n Schubladen zu verteilen, so gibt es eine Schublade mit mehr als einem Gegenstand. Prüfen sie für konkretes n (2,3) die Allgemeingültigkeit der Formel.

6. "Es kann dauern ohne Optimierung ... "(Schubladenformel verpackt in tertium non datur)

   or or - and and or a - - b or c - - d or e - - g or or or or or and a c and a e and c e and b d and b g and d g - or - and and or a - - b or c - - d or e - - g or or or or or and a c and a e and c e and b d and b g and d g