Logica voor informatica

Website:

website met extra informatie

Vakcode:

INFOB1LI

Studiepunten:

7.5 ECTS

Periode:

periode 2 (week 46 t/m 5, dwz 15-11-2010 t/m 4-2-2011; herkansing week 11)

Timeslot:

Deelnemers:

tot nu toe 220 inschrijvingen

Rooster:

Let op: m.i.v. het collegejaar 2008/2009 is het rooster te vinden in Osiris

Docenten:

Dit is een oud rooster!

vorm	groep	tijd	week	zaal	docent
college	groep 4	ma 13.15-15.00	46-48	BBL-061	Jan van Leeuwen
			49	DDW-1.30
			50	BBL-061
			2	BBL-061
			3-4	AARD-GROOT
		di 15.15-17.00	46-50	BBL-065
		di 15.15-17.00	2-4	BBL-169
	groep 12356	ma 15.15-17.00	46-50	AARD-GROOT	Jan van Leeuwen
		ma 15.15-17.00	2-4	AARD-GROOT
		do 9.00-10.45	46-50	AARD-GROOT
		do 9.00-10.45	2-4	AARD-GROOT
coordinatie					Peter de Waal
werkcollege	groep 1	di 13.15-15.00	47-50	BBL-017	Mehdi Dastani Vincent Kreuzen
		di 13.15-15.00	2-4	BBL-017
		do 11.00-12.45	46-51	BBL-005
		do 11.00-12.45	2-4	BBL-005
	groep 2	di 13.15-15.00	47-50	BBL-075	Mehdi Dastani Wout Elsinghorst
		di 13.15-15.00	2-4	BBL-075
		do 11.00-12.45	46-51	BBL-075
		do 11.00-12.45	2-4	BBL-075
	groep 3	di 13.15-15.00	47-50	BBL-077	Mehdi Dastani Thijs Alkemade
		di 13.15-15.00	2-4	BBL-077
		do 11.00-12.45	46-51	BBL-077
		do 11.00-12.45	2-4	BBL-077
	groep 4	di 13.15-15.00	47-50	BBL-065	Marinus Veldhorst Ruud Koot
		di 13.15-15.00	2-4	BBL-065
		do 11.00-12.45	46-51	BBL-079
		do 11.00-12.45	2-4	BBL-079
	groep 5	di 13.15-15.00	47-50	BBL-201	Peter de Waal Remco Mol
		di 13.15-15.00	2-4	BBL-201
		do 11.00-12.45	46-51	WISK-611AB
		do 11.00-12.45	2-4	WISK-611AB
	groep 6	di 13.15-15.00	47-50	MIN-021	Merel Rietbergen Wouter van Toll
		di 13.15-15.00	2-4	MIN-021
		do 11.00-12.45	46-51	MIN-207
		do 11.00-12.45	2-4	MIN-207

Tentamen:

week: 51	do 19-12-2013	8.30-10.30 uur	zaal: EDUC-BETA
week: 5	do 30-1-2014	8.30-10.30 uur	zaal: EDUC-BETA

Inhoud:

Voor welke doel we ook een programma ontwerpen, altijd moeten we ons rekenschap geven van de eisen die aan een programma gesteld worden, resp. van de eigenschappen die het resulterende programma heeft. Hoe formuleren we uitspraken over programmas als deze? Hoe bepalen we of een uitspraak geldt? Zou dat altijd mogelijk zijn? Hoe zit het redeneren met formele eigenschappen in elkaar en, kan het misschien door speciale programmas voor ons gedaan worden?

Het college bestaat uit de volgende onderdelen:

verzamelingen: bewerkingen, afbeeldingen, relaties, aftelbare en overaftelbare verzamelingen, bewijzen met inductie.
berekenbaarheid: beslisbare (`berekenbare') verzamelingen versus onbeslisbare, dito voor eigenschappen van programmas, Church-Turing these.
formele systemen: ingredienten van elke logica, deductie, bewijsbare formules, modellen, ware formules, consistentie.
propositielogica: basisprincipes van redeneren met proposities, conjunctieve en disjunctieve normaalvorm, axiomatisering, volledigheid, complexiteit (P versus NP).
1ste orde predicatenlogica: syntax, redeneren met formules (`uitspraken'), expressiviteit, algemeen geldigheid, principe van automatic theorem proving en `logic programming', axiomatisering, volledigheidstelling, complexiteit.
toegepaste logica (in aanvulling op toepassingen in de eerder genoemde onderdelen, selectie): redeneren over programmas (Floyd-Hoare logica), programmaverificatie, model checking, kennisrepresentatie, query talen, etc.

Leerdoelen: vertrouwd raken met de principes van de logica, het onderscheid tusen syntax en semantiek, het kunnen formuleren van uitspraken in propositie- of predicaatlogica, het kunnen maken van eenvoudige berekeningen met formules zoals deductie en resolutie, het begrijpen en hanteren van de kerneigenschappen van logicas, het redeneren over programmas, kennismaking met begrippen rond complexiteit en (on)beslisbaarheid van eigenschappen in de informatica.

Literatuur:

Het college wordt nieuw ontwikkeld en maakt dit jaar nog niet gebruik van een specifiek boek. Collegemateriaal wordt op de website van het college gepost in pdf. Deelnemers worden geacht dit materiaal zelf te downloaden resp af te drukken en bij college en werkcolleges paraat te hebben.

De per keer behandelde onderwerpen en bijbehorende documentatie worden vermeld in het weekgewijze werkschema op de website met `extra informatie'.

Aanvullende literatuur ter naslag staat vermeld op de website met `extra informatie'.

Werkvorm:

Per week: 4 uur hoorcollege (2 zittingen van 2 uur) en 4 uur werkcollege (2 zittingen van 2 uur). Per keer moeten in het werkcollege enkele oefenopgaven en/of een opdracht worden gemaakt. Gedurende het blok moet drie keer een opdracht worden ingeleverd. Deelname aan de werkcolleges wordt geregistreerd.

LET OP: In verband met het verwachte deelnemeraantal wordt het hoorcollege wekelijks `dubbel' gegeven. De deelnemers aan het college worden daarom in twee groepen ingedeeld: groep A (tot 150 deelnemers) heeft college op maandag (15.15-17.00) en donderdag (9.00-10.45), groep B (tot 55 deelnemers) heeft college op maandag (13.15-15.00) en dinsdag (15.15-17.00). Bij welke groep je bent ingedeeld staat vermeld op de website met `extra informatie'.

De werkcolleges worden in 6 groepen ingedeeld. Bij welke werkcollegegroep je bent ingedeeld staat op de website met `extra informatie'.

Toetsvorm:

De beoordeling van het college bestaat uit drie onderdelen: het werkcollege (W) en twee deeltentamens (T1, T2). Het werkcollege wordt beoordeeld op deelname en prestatie in de wekelijkse sessies (50%) en de drie opdrachten (50%). (Zie de website met `extra informatie' voor een nadere detaillering.) Het deeltentamens betreffen: een toets (T1) halverwege over de eerste helft van de collegestof, en een toets (T2) aan het eind over de tweede helft van de stof (ook met begrippen uit het eerste deel).

Het totaalcijfer wordt berekend als: 0.2*W + 0.3*T1+0.5*T2. Deelcijfers worden in een cijfer achter de komma gehouden, maar het totaalcijfer wordt afgerond: op halven boven de zes en op helen onder de zes, dus 5.5 wordt 6 en 5.4 wordt 5. Als een van de deelcijfers ontbreekt blijft het vak `onvoltooid'.

Eventueel kan een aanvullende toets worden gedaan, op de voorziene datum in de herkansingsweek tijdens de volgende periode. Het cijfer hiervoor kun je alleen inzetten voor een van T1, T2 (om een onvoldoende of een ontbrekend cijfer te vervangen). De aanvullende toets gaat over de hele stof, ongeacht voor welk van de twee deelcijfers hij als vervanging geldt.

Inspanningsverplichting voor aanvullende toets:

Om aan de aanvullende toets te mogen meedoen moet je minimaal het werkcollege hebben voltooid en aan ten minste een van de twee toetsen hebben meegedaan.

Beschrijving:

Het college geeft een inleiding tot de logica, de klassieke wetenschap die zich bezighoudt met de theorie en toepassing van het correct redeneren, ihb dus voor toepassing op uitspraken over (eigenschappen van) programmas en systemen in de informatica.

De logica biedt talen voor het formuleren van `uitspraken en eigenschappen', methoden voor systematisch redeneren (bijv. over programmacorrectheid), en mechanismen voor intelligente systemen. Er is vaak een direct verband met het redeneren met behulp van programmas zelf, en het direct oplossen van problemen die in logische formules zijn gespecificeerd. Bewijsbaarheid, oplosbaarheid en berekenbaarheid zijn daarmee vaak, maar niet altijd, keerzijden van dezelfde medaille.

De `formele' logica levert concepten en inzichten die juist in de informatica hun `dynamische' vorm vinden. Omgekeerd kent de informatica vele probleemstellingen en modelleringen die met behulp van begrippen en technieken uit de logica het best kunnen worden geanalyseerd. En zo moet het idealerwijze ook zijn: formele methoden moeten ontwerpers helpen.

wijzigen?