Existenzquantoren entfernen mit Skolemfunktionen

Existenzquantoren lassen sich mithilfe von Funktionen ausdrücken. Diese sogenannte Skolemisierung (nach Thoralf Skolem, 1920) ist ein wichtiger Vorbereitungsschritt für den Resolutionsalgorithmus. Dazu führen wir noch kurz Funktionssymbole in die Prädikatenlogik ein und besprechen, inwiefern sich dadurch (nicht) die Ausdrucksstärke erhöht.
► Playliste für diesen Videokurs: • Theoretische Informati...
► Vorlesungsfolien zum Download: iccl.inf.tu-dresden.de/web/Th... (17. Vorlesung)
► Aktuelle und frühere Versionen der Vorlesung: iccl.inf.tu-dresden.de/web/Th...
► Fehler gefunden? Issues melden auf github: github.com/knowsys/TheoLog
Literaturempfehlungen:
► Hao Wang: Skolem and Gödel. Nordic Journal of Philosophical Logic, Vol. 1, No. 2, pp. 119-132. www.hf.uio.no/ifikk/forskning/...
tidsskrifter/njpl/vol1no2/skogod.pdf
► Thoralf A. Skolem: Logisch-kombinatorische Untersuchungen über die
Erfüllbarkeit und Beweisbarkeit mathematischen Sätze nebst einem Theoreme über dichte Mengen. Videnskapsselskapets Skrifter. I. Mat.-naturv Klasse, 1920, No. 4. Kristiania 1920.
Bildrechte: Portrait Skolem, 1930er (heute Oslo Museum, Inventarnummer OB.F06426c), gemeinfrei

[@LarsL-qy7pj]

Wirklich gut erklärendes video, und auch sehr toll, dass es den kram über git gibt. In Kiel macht man momentan parallel Prolog, und die Technik am Ende um Funktionen über Prädikate zu implementieren hat in meinem Gehirn eine tolle Brücke dazu geschaffen. Danke :)