Semantics of Logic Programming (IBC012). De vakbeschrijving.

Werkcollege: Woensdag 10:30 - 12:30 (wk 46-51, HFML0220)

Hoorcollege: Vrijdag 8:30 - 10:30 (wk 46-51, HFML0220)

Tentamen: Vrijdag 11 jan: 8:30 - 10:30 (Hg00.304)

Hertentamen: Maandag 24 juni 9:31 - 11:30 (HG00.062)

Deze pagina wordt geduurde het college aangepast.

Voorbereidingen

Tijdens het vak maken we de opgaves in Proofweb (proofweb). Bij problemen kun je contact opnemen met Kasper Brink (k.brink@cs.ru.nl).

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. Een document om de transitie van B en B naar Proofweb te vergemakkelen.). Je kunt de opgaves ook offline maken. Upload de opgaves als je klaar bent. Gebruik deze file. Dan:
tar xvzf proofweb_exercises.tar.gz
cd proofweb
coqc ProofWeb.v
coqide prop_001.v

Week 1 (14,16,21 nov)

Afleidingen in propositie- en predicatenlogica Zowel 16 als 21 nov is er werkcollege. Op beide dagen is er gelegenheid vragen te stellen over Proofweb.

Week 2 (23,28 nov)

Modellen van de Propositie- en Predicatenlogica.

Week 3 (30 nov, 5dec)

Clausules en Unificatie.

Week 4 (7 dec,12dec)

Algemene resolutie en "normalizatie" van formules

Week 5 (14 dec, 19 dec)

SLD-resolutie en Herbrandmodellen. Prolog-voorbeeld en uitleg.

Week 6 (21 dec, 9jan)

Onvolledigheid

Vragenuur 9 Januari.


Literatuur:
Logica voor Informatica.
Reeves and Clarke - Logic for computer science Ch5,6,7.
Voorbeeld tentamens zijn hier te vinden.
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.