Semantics of Logic Programming (IBC012)
De vakbeschrijving.
Docent: Herman Geuvers
Colleges: Woensdag 10:30 - 12:30 (wk 46-03, HG00.071) en
Vrijdag 15:30 - 17:30 (wk 46-03, HG00.068)
Tentamen: Maandag 27 jan: 8:30 - 11:30 (LIN 4)
Hertentamen: Dinsdag 4
maart: 12:30 -15:30, HG01.028
NB: Deze pagina wordt geduurde het college aangepast.
Inhoud
Tijdens het vak maken we de opgaven in Proofweb (proofweb).
- Voor een login in proofweb: stuur de docent een mail met subject [soflp] en als inhoud username=password=studentnummer. (Dus je kiest zelf een username en password.)
- Proofweb werkt alleen goed met de Firefox browser, dus installeer deze eerst.
- Bij problemen kun je contact opnemen met Kasper Brink (k.brink@cs.ru.nl).
-
Je kunt de opgaven ook offline maken op je eigen laptop/pc. Upload de opgaven als je klaar bent:
- Gebruik deze file.
- Voordat deze opdrachten gebruikt kunnen worden moet je eerst "coqc
BenB.v" doen in de exercises directory om een .vo file te maken.
De opgaven op Proofweb zijn bedoeld om de vaardigheden die je in andere
vakken, zoals beweren en bewijzen, hebt geleerd te testen en voor je
zelf te automatiseren. Het is cruciaal dat deze
afleidingen in de rest van het vak vanzelf gaan.
Bepaal voor jezelf hoeveel oefening je nodig hebt. (De B-en-B bewijsstrategie (of hier 1,2,3)
en Deductie-regels.)
Thema 1 (13,15 nov)
Afleidingen in propositie- en predicatenlogica
Op 15 nov is er werkcollege. Er is gelegenheid vragen te stellen over Proofweb.
NB op 20 nov is er geen college!
Thema 2 (22,27 nov)
Modellen van de Propositie- en
Predicatenlogica.
Thema 3 (29 nov, 4 dec)
Clausules en Unificatie.
Thema 4 (8 dec,11 dec)
Algemene resolutie en "normalizatie" van formules
Thema 5 (13 dec, 18 dec)
SLD-resolutie en Herbrandmodellen.
Thema 6 (20 dec, 8 jan)
Onvolledigheid
Vragenuur 10 Januari.
Literatuur:
Logica voor Informatica en aantekeningen die bij de leertaken verspreid worden. (In het Engels is er ook Reeves and Clarke: Logic for computer science Ch5,6,7.).
Het tentamen van 2009 (uitwerking) en het hertentamen.
Het tentamen van 2010 met uitwerkingen.
Het cijfer van het tentamen is je eindcijfer. Het tentamen is open boek.