Prof. Dr. M. Kreuzer Abgabe: 05.01.2004, 12.15 Uhr Peter Ackermann

Logik für Informatiker

Übungsblatt 10

Aufgabe 23: Beim Rentiergespann des Weihnachtsmannes verhält es sich so, dass die Rentiere in Paaren vor den Schlitten gespannt sind. Dabei gilt, dass die Väter zweier Rentiere, die ein Paar bilden, wiederum ein Paar bilden (d. h. der Partner des Vaters ist der Vater des Partners).

a) Formulieren Sie diese Situation mit Hilfe von gleichungslogischen Formeln (Hinweis: Man drücke aus, dass der Partner des Partners eines Rentiers das Rentier selbst ist).

b) Zeigen Sie, dass das zugehörige Termersetzungssystem Noethersch und konfluent ist.

c) Zeigen Sie, dass der Partner des Vaters des Partners eines Rentiers der Vater dieses Rentiers ist.

Aufgabe 24: Die ganzen Zahlen seien dargestellt durch die Konstante 0 sowie die einstelligen Funktionen s (wie successor) und p (wie predecessor). So sei etwa −3 durch p(p(p(0))) und 2 durch s(s(0)) repräsentiert. Weiterhin ordne m einer Zahl z die Zahl −z zu. Betrachte die Menge gleichungslogischer Formeln

1. s(p(x)) = x

2. p(s(x)) = x

3. m(0) = 0

4. m(s(x)) = p(m(x))

a) Zeigen Sie, dass das zugehörige Termersetzungssystem Noethersch ist.

b) Vervollständigen Sie das Termersetzungssystem.

c) Zeigen Sie, dass gilt p(m(p(x))) = m(x).

Frohes Fest und guten Start ins neue Jahr!!!