Beweren en Bewijzen

Inleiding

Hoe bereikt men helderheid? Wanneer is een bewering waar? Wanneer doet een ICT-systeem wat het moet doen? We beschouwen verschillende toepassingsgebieden van taal, bijvoorbeeld juridische wetten en contracten. Voor informatici belangrijke speciale gevallen zijn specificaties (als contract) en algoritmen (uitvoeringsvoorschriften). We gaan uit van uitspraken in natuurlijke taal. Deze gaan we
  • analyseren en beperken tot constructies die we echt begrijpen, en
  • formaliseren, d.w.z. in een notatie gieten met een goed gedefinieerde betekenis.
Vervolgens gaan we
  • bestuderen aan welke regels deze formele uitspraken onderhevig zijn en hoe men tot aantoonbaar ware uitspraken kan komen,
  • dit toepassen op de ontwikkeling en validatie van systemen die doen wat ze moeten doen,
  • dit alles exemplarisch vergelijken met benaderingen, gebaseerd op enige andere formalismen.

Leerdoelen

Na afloop van de cursus kun je:

  1. 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
  2. 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
  3. 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
    • het verband aangeven tussen logische en enkele andere specificatieformalismen

Onderwerpen

Realiteit, abstractie, modellen, contracten, verborgen aannames, natuurlijke en formele talen, syntaxis en semantiek, typering, propositie- en predikaatlogica, waarheidstabellen, semantische tableaus, natuurlijke deductie, specificatie, correctheid van systemen, Chinese dozen (hiërarchische decompositie), bewijsassistenten

Werkvormen

  • 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 elektronische werkplaats werken we samen aan grote projecten en wekelijkse opdrachten. We formuleren in natuurlijke taal zo precies mogelijk wat een bepaald ICT-systeem moet doen (bijvoorbeeld botsingen tussen treinen en auto's voorkomen) en zetten deze specificatie vervolgens om in een formele taal: de predikaatlogica. Daarbij komen we vanzelf allerlei ambiguïteiten tegen; de logica dwingt ons, deze op te lossen. We specificeren op dezelfde manier de aannames die we redelijkerwijs kunnen maken over de onderdelen van zo'n systeem (slagbomen, treinen, besturingskastje, wegenwet). Als alles klopt en goed in elkaar zit, moet formeel bewezen kunnen worden dat het systeem inderdaad aan zijn specificatie voldoet. Om de studietaken competent uit te voeren oefen je in zelfstudie iedere week met de nieuwe stof uit de hoorcolleges. In de responsiecolleges bespreek je klassikaal je eigen oplossing en die van anderen. Je mag alleen naar de responsiecolleges komen indien de bijbehorende leertaak serieus is ingeleverd.

Toetsvorm

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 sommige 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.
    • Voor het gemiddelde van de deeltentamens moet je minimaal een 5.5 hebben. 
    • Indien je aan beide eisen voldaan hebt is je theoriecijfer het gemiddelde van de deeltentamens.
    • Indien je niet aan beide eisen 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.5 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.

Vereiste voorkennis

Je moet vertrouwd zijn met het verschil tussen een informele en een formele benadering op het niveau van de cursussen Formeel Denken, Wiskundige Structuren of een vergelijkbare cursus. Enige ervaring met een aantal formele programmeer- en modelleringstalen (en dus ook met programmeren en modelleren zelf) is gewenst.

Literatuur

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.

Bijzonderheden

Website


Vakcode
NWI-IPI004
Studiepunten
6 ec
Periode
tweede semester

Docenten

Opgenomen in