| Na afloop van de cursus kunt je:
- Algemene bekwaamheden
- inconsistenties en incorrectheden aanwijzen in niet deugende uitspraken
- heldere, consistente en correcte uitspraken formuleren
- de correctheid van eigen beweringen beredeneren
- oplossingen systematisch afleiden c.q. een systematische afleiding presenteren
- actief en constructief meewerken aan het verhelderen van onduidelijke uitspraken
- teksten en discussies structureren d.m.v. begripsdefinities
- het onderscheid aangeven tussen natuurlijke taal en formele talen
- professioneel omgaan met verschillende notaties voor dezelfde taal
- Specifieke bekwaamheden logica
- herkennen welke redeneerproblemen met propositielogica kunnen worden aangepakt en welke niet
- beweringen in natuurlijke taal omzetten naar logica
- de betekenis van logische formules helder in natuurlijke taal weergeven
- de betekenis van de regels voor natuurlijke deductie aangeven
- eenvoudige beweringen bewijzen met behulp van natuurlijke deductie
- bewijzen netjes opschrijven
- voor gegeven beweringen in propositielogica een waarheidstabel opstellen
- voor gegeven beweringen in propositielogica een semantisch tableau opstellen
- voor gegeven beweringen in propositielogica aangeven of het een tautologie, een equivalentie of een logisch gevolg betreft
- redeneerfouten herkennen en blootleggen
- de bewijsassistent Coq gebruiken om stellingen mee te bewijzen
- Specifieke bekwaamheden systeemontwikkeling
- een rationaliteitsvierkant opstellen bij een artefact
- relevante eigenschappen van eenvoudige ingebouwde real-time-systemen en hun onderdelen logisch specificeren
- de juistheid van logische specificaties aantonen
- systemen hiërarchisch onderverdelen
- op basis van logische specificaties bewijzen dat een uit de juiste onderdelen samengesteld systeem de verlangde eigenschappen heeft
- systeemanalyse, systeemontwerp en correctheidsbewijs helder presenteren
|
 |
| Dit is een cursus toegepaste logica. Enerzijds leer je systemen te beschrijven, zowel op informele wijze in natuurlijke taal als op formele wijze in propositie- of predikaatlogica. Hierbij is het doel om de beschrijvingen zo duidelijk te maken dat ze als een contract kunnen dienen. Anderzijds leer je hoe je kunt bewijzen dat systemen doen wat ze moeten doen volgens hun specificatie. Ook dit gaat weer in natuurlijke taal en in wiskundige taal met formele methoden. Uiteindelijk zelfs met een bewijsassistent die het bewijs controleert.
De technieken worden geoefend in relatief kleine wekelijkse leertaken. En ze worden getoetst via schriftelijke deeltentamens en een groepswerkstuk waarin je aan de hand van een complex systeem laat zien dat je alle facetten van het beweren en het bewijzen beheerst. |
|
|
|
Dit zijn de belangrijkste onderwerpen:
• Het rationaliteitsvierkant.
• De focus van een model.
• Natuurlijke talen en formele talen.
• Propositielogica en predikaatlogica: syntax en semantiek.
• Systematische vertaalmethode van natuurlijke taal naar predikaatlogica.
• Bewijzen in natuurlijke taal.
• Bewijzen in formele taal: met waarheidstabellen, semantische tableaus en natuurlijke deductie.
• Werken met een bewijsassistent.
• Correctheidsstelling van een systeem. |
|
Onderdelen van de toetsing
• Leertaken.
• Bijna elke week is er een leertaak waarin je aan de slag gaat met de theorie uit het hoorcollege.
• Deze leertaken zijn niet verplicht, maar voor de meeste studenten essentieel om de stof goed te begrijpen.
• Je krijgt voor deze leertaken een beoordeling.
• Je leertaakcijfer is het gemiddelde van deze beoordelingen.
• Je bonuscijfer is je leertaakcijfer gedeeld door 10.
• Bij veel leertaken dienen opdrachten met Coq te worden gedaan. Die opdrachten zijn dan onderdeel van het hieronder genoemde verplichte Coq-practicum.
• Verplicht Coq-practicum.
• Gedurende het semester zijn er individuele opdrachten die met Coq gemaakt moeten worden.
• Je krijgt voor deze opdrachten een beoordeling.
• Je Coqcijfer is het gemiddelde van al die beoordelingen.
• Je Coqcijfer dient aan het eind van het semester minstens 5.5 te zijn om een voldoende te kunnen krijgen.
• Deeltentamens.
• Er zijn twee schriftelijke deeltentamens.
• Voor elk deeltentamen moet je minimaal een 5.0 hebben.
• Indien je aan die eis voldaan hebt is je theoriecijfer het gemiddelde van de deeltentamens.
• Indien je niet die eis voldaan hebt is je theoriecijfer het minimum van het gemiddelde van de deeltentamens en een 5.
• Werkstuk.
• Je maakt een (groeps)werkstuk waarin je laat zien dat je de theorie kunt toepassen.
• Het werkstuk wordt in twee delen ingeleverd.
• Voor het eerste deel krijg je geen cijfer maar een 'voldaan' of 'niet voldaan'.
• Om een compleet werkstuk te mogen inleveren dien je natuurlijk een 'voldaan' te hebben voor het eerste deel.
• Voor het complete werkstuk krijg je een gewoon cijfer, het werkstukcijfer.
• Om het vak te halen moet je werkstukcijfer minstens een 5.5 zijn.
Eindcijfer
• Indien Coqcijfer minimaal 5.5 en theoriecijfer minimaal 5.0 en werkstukcijfer minimaal 5.5 dan geldt:
• eindcijfer = (theoriecijfer + werkstukcijfer) / 2 + bonuscijfer.
• In alle andere gevallen geldt:
• eindcijfer = minimum( 5 , (theoriecijfer + werkstukcijfer) / 2).
• Eindcijfers worden afgerond conform de eisen van de administratie.
Herkansingen
• De leertaken zelf kunnen niet herkanst worden.
• Indien je voor het Coq-practicum een gemiddelde tussen de 5 en 5.5 hebt, mag je dit Coq-practicum herkansen aan het eind van het semester.
• Voor het eerste deel van het werkstuk geldt dat indien je niet meteen een 'voldaan' hebt behaald, er enkele weken later een herkansing is voor dat deel. Levert dat nog steeds geen 'voldaan' op, mag je geen werkstuk meer inleveren en haal je dus het vak niet, maar je mag nog wel de deeltentamens maken. Onder bepaalde voorwaarden mag je die deeltentamens dan in het volgende jaar hergebruiken.
• Alle deeltentamens waarvoor een cijfer lager dan 5.5 is gehaald, mogen aan het eind van het semester herkanst worden, tenzij het afgeronde eindcijfer al een 6.0 of hoger is.
• Indien voor het complete werkstuk een cijfer lager dan 5.5 is gehaald, mag dit werkstuk aan het eind van het semester herkanst worden. |
|
| Je dient basiskennis te hebben van propositielogica en predikaatlogica op het niveau van de cursussen Formeel Denken (IPK001) of Wiskundige Structuren (IPC020). Daarnaast is het praktisch als je enige ervaring hebt met programmeren en modelleren. |
| Aangeraden: een leerboek over predikaatlogica en natuurlijke deductie, bijvoorbeeld J.F.A.K. van Benthem et al.: Logica voor informatica; Pearson Education Benelux, 2003, ISBN 90-430-0722-6. Het is een boek waar je ook later nog veel aan kunt hebben. In deze cursus gebruiken we er alleen bepaalde onderdelen van. Je mag ook oudere oplagen of een ander boek gebruiken. |
|
• 3 uur begeleid groeps project werk
• 32 uur hoorcollege
• 27 uur onbegeleid groeps project werk
• 16 uur responsie-college
• 90 uur zelfstudie
Toelichting werkvormen: In de hoorcolleges worden de nieuwe onderwerpen uitgelegd.Vervolgens zijn er wekelijkse individuele leertaken waarbij geoefend wordt met de nieuwe theorie. Ook wordt er bijna elke week geoefend met de bewijsassistent Coq. Alleen indien de leertaak serieus is ingeleverd, mag men naar de responsiecolleges komen om feedback over de opgaven te krijgen.
Er worden geen standaarduitwerkingen van de leertaken verstrekt: studenten zullen zelf actief mee moeten doen om te checken of hun uitwerkingen correct waren.Daarnaast wordt er een groot werkstuk gemaakt. In dit werkstuk wordt een bepaald artefact gekozen, waar een compleet model van gemaakt wordt. Dit model bevat onder andere specificaties van de verschillende onderdelen en van het geheel, zowel in natuurlijke taal als in predikaatlogica. Ten slotte bevat het werkstuk een correctheidsstelling die aangeeft dat het artefact precies werkt zo als gewenst, indien het uit geschikte onderdelen is samengesteld. Deze correctheidsstelling wordt met natuurlijke deductie in een bewijsassistent bewezen. |
|
| | Aanbevolen materiaalBoek| J.F.A.K. van Benthem et al.: Logica voor informatica; Pearson Education Benelux, 2003 |
| Boek| Logic in Computer Science, by Huth and Ryan (Engels) |
|
|
WerkvormenCursusgebeurtenis
| Hoorcollege
| Project
| Responsiecollege
| Zelfstudie
|
|
ToetsenTentamen| Weging | | 1 |
| Gelegenheden | | Blok KW4, Blok KW4 |
|
|
| |