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 Informatik und Logik (B.Sc.-N...  
► Vorlesungsfolien zum Download: https://iccl.inf.tu-dresden.de/web/Th... (17. Vorlesung)
► Aktuelle und frühere Versionen der Vorlesung: https://iccl.inf.tu-dresden.de/web/Th...

► Fehler gefunden? Issues melden auf github: https://github.com/knowsys/TheoLog


Literaturempfehlungen:
► Hao Wang: Skolem and Gödel. Nordic Journal of Philosophical Logic, Vol. 1, No. 2, pp. 119–132. http://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