Logik:Klausuren/25.07.2003/4 Aufgabe
Inhaltsverzeichnis
1. Aufgabenstellung
Sei $ Q $ ein Qunator und $ F' $ eine Formel, in der die Variable $ X $ nicht frei vorkommt. Dann heißt $ (QX) $ ein leerer Quantor für die Formel $ F = (QX)F' $.
a) Beweisen Sie, dass in diesem Fall $ F $ und $ F' $ semantisch äquivalent sind.
b) Schreiben Sie ein Prolog-Programm rv/2, das im ersten Argument eine prädikatenlogische Formel erwartet und im zweiten Argument eine semantisch äquivalente Formel ohne leere Quantoren zurückgibt. Nehmen Sie dazu an, dass Formeln zusammengesetzt sind aus Allquantoren in der Form all(x, formel) sowie dem vordefinierten Operatoren not/1 und and/2. Außerdem dürfen Sie das bekannte Prädikat member/2 sowie ein vordefiniertes Prädikat freevars/2 verwenden, das für jede im ersten Argument gegebene Formel eine Liste der darin enthaltenen freien Variablen im zweiten Argument zurückgibt.
2. Lösung
a)
$ F^{I,Z} = ((QX)F')^{I,\mathcal{Z}} = F'^{I, \{X \mapsto d\} \mathcal{Z}} $ für alle $ d \in D $ falls $ Q = \forall $ oder für ein $ d \in D $ falls $ Q = \exists $
$ =F'^{I,\mathcal{Z}} $, da $ X $ in $ F $ nicht vorkommt.
