practicum 8 (maandag 7 november 2011)
Er zijn geen practicumopgaven. Er zijn van 13:15 tot 15:00 studentassistenten aanwezig in 1.02 om vragen over de stof te beantwoorden.practicum 7 (maandag 31 oktober 2011)
Dit practicum is een werkcollege.Opgaven uit hoofdstuk 8.
- Op de werkgroep te behandelen:
1d,e,f,j,k,l,m,o,p - Inleveren op maandag 7 november:
1q,r,s,t,u,v
practicum 6 (maandag 24 oktober 2011)
Opgavenpracticum 5 (maandag 17 oktober 2011)
Opgaven te doen mbv een eenvoudig tool, gemaakt door Jan Jaspars, om eenvoudige werelden (bestaande uit ten hoogste 4 personen, twee eigenschappen, en een relatie) te maken en te bepalen of predikaatlogische formules waar zijn voor zo'n wereld.practicum 4 (maandag 10 oktober 2011)
Vragenuur als voorbereiding op tussentoets.practicum 3 (maandag 3 oktober 2011)
Opgaven uit Hoofdstuk 8 op te lossen doen m.b.v. yices (d.w.z. modelleer de problemen steeds als satisfiability problemen, geef die aan yices, en leg uit hoe de uitkomst van yices de vraag beantwoordt).- Op practicum te doen: 2(ii,v), 6(ii,v), 7(ii,v), 9, 11
- In te leveren (maandag 10 oktober): 2(iv), 6(iv), 7(iv), 10
practicum 2 (maandag 26 september 2011)
Practicumopgaven over satisfiability te doen m.b.v. yices (download) als getoond op het hoorcollege. Het programma is al geinstalleerd op de practicumcomputers, zie de yices instructie van ICT en Media, over hoe je het kunt gebruiken. Een vb is op het college behandeld, nl of A een semantisch gevolg van A & B is. Daartoe kan gecheckt worden of de verzameling { A & B, niet A } strijdig is. Deze verzameling wordt gecodeerd in het bestand test.smt die je in je homedirectory (zie je loginnaam onder places in een finder window) dient te plaatsen. Om te checken of de formule strijdig is (dwz onvervulbaar) tik je vervolgens in een terminal in:yices -smt -e test.smt
gevolgd door een return. (als het goed is zegt hij unsat.)
- Op practicum te doen van hoofdstuk 7: 7(i,ii),9(iii),9(iv),11(vi), b.v. door steeds het eerdere bestand test.smt te kopieren en geschikt aan te passen.
- In te leveren (maandag 3 oktober) van hoofdstuk 7: 7(iii),8(iv),9(i),9(ii),11(v).
-
(voor liefhebbers) Schrijf een formule die willekeurige Sudoku’s oplost
(het is een lange basis formule die per sudoko aangevuld wordt met extra condities).
Om dit op te lossen kunt u in stappen te werk gaan, b.v.:
-
Bedenk eerst proposities die aangeven welk cijfer op welke coordinaat staat,
b.v. zou je
p003als propositie die uitdrukt dat op coordinaat 0,0 van de sudoku het cijfer 3 staat, kunnen nemen. -
Druk vervolgens de eisen die op sudoku's gelden uit m.b.v. formules in de propositielogica.
B.v.
p001 \/ ... \/ p009drukt uit dat op coordinaat 0,0 een van de cijfers 1 t/m 9 moet staan; -
Druk vervolgens de beginsituatie van een concrete sudoku uit.
B.v.
p114 /\ p215drukt uit dat op er een 4 staat op coordinaat 1,1 en eeb 5 op coordinaat 2,1; - Neem de conjunctie van alle eisen en de beginsituatie (een hele grote formule), voer die geschikt in yices in en laat yices z'n werk doen.
-
Bedenk eerst proposities die aangeven welk cijfer op welke coordinaat staat,
b.v. zou je
practicum 1 (maandag 19 september 2011)
Practicumopgaven te doen m.b.v. de waarheidstabulator Op dit practicum te behandelen: Hfdstk 5: 1(i),1(ii),3; (ii),(iv),(vi) Na te bespreken op werkgroep: Hfdstk 5: 3(vii); In te leveren (volgende week maandag tezamen met werkgroepopgaven) Hfdstk 5: 3(i),(iii),(v). Druk de uitvoer van het programma af, en schrijf daar eventueel verder benodigde antwoorden bij. (Voorzie wat u inlevert altijd van uw naam, studentnr, en ook werkgroepnr.)Inleveropgaven dienen zelfstandig gemaakt te worden. Onderdelen van de opgegeven sommen uit de syllabus die noch bij de werkgroepopgaven noch bij de inleveropgaven voorkomen, kunt u natuurlijk zelf (buiten de werkgroepen) maken. Ook over die opgaven kunt u desgewenst vragen stellen tijdens de werkgroepen.