IDENK1 (IDENK1)
Beweren en Bewijzen*
< 2006/2007 > 05-02-2007 t/m 01-07-2007 (15-07-2007) L
Informatica - Bachelor (2003) Gegevens: Informatie- en kennissystemen (1 ec) Omgeving (2 ec) Grondslagen (3 ec)
Informatica - Master na HBO Artificial Intelligence variant MT (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Artificial Intelligence variant O (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Computer Security variant MT (2003) Schakelcursussen (6 ec)
Informatica - Master na HBO Computer Security variant O (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Embedded Systems variant MT (2003) Schakelcursussen (6 ec)
Informatica - Master na HBO Embedded Systems variant O (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Information Systems variant MT (2003) Schakelcursussen (6 ec)
Informatica - Master na HBO Information Systems variant O (2004) Schakelcursussen (6 ec)
Informatica - Master na HBO Software Construction variant MT (2003) Schakelcursussen (6 ec)
Informatica - Master na HBO Software Construction variant O (2004) Schakelcursussen (6 ec)
Informatiekunde - Bachelor (2003) Grondslagen (6 ec)
Informatiekunde na het HBO (2003) Schakelvakken (6 ec)
omvang
6 ec (168 uur) : 40 uur plenair college, 40 uur groepsgewijs college, 0 uur computerpracticum, 20 uur 'droog' practicum, 2 uur gesprekken met de docent, 10 uur onderling overleg met medestudenten (werkgroepen, projectwerk e.d.), 56 uur zelfstudie
investering
6 ec * 28 u/ec + #std * (1 + 6ec * 0.75 u/student/ec)
inzet tentatief

docent
afdeling
tijdbesteding

prof. dr. Erik Barendsen
sws
100u.

docent
afdeling
tijdbesteding

dr. Stijn Hoppenbrouwers
sws
50u.

docent
afdeling
tijdbesteding

dr. Engelbert Hubbers
dis
100u.

speciale web-site
https://wiki.science.ru.nl/IIwerkplaats/BenB

 

Hoe bereikt men helderheid? Wanneer is een bewering waar? Wanneer doet een ICT-systeem wat het moet doen? We beschouwen verschillende toepassingsgebieden van taal, juridische wetten bijvoorbeeld, en contracten. Voor informatici belangrijke speciale gevallen zijn specificaties (als contract) en algoritmen (uitvoeringsvoorschriften, speciale gevallen van een speciaal geval van wetten). 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 (SQL, state based systems).

Leerdoelen

Algemene bekwaamheden

  • inconsistenties en incorrectheden aanwijzen in niet deugende uitspraken
  • heldere, consistente en correcte uitspraken formuleren
  • de correctheid van eigen beweringen beredeneren
  • oplossingen systematisch kunnen 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 kunnen aangeven tussen natuurlijke taal en formele talen
  • professioneel kunnen omgaan met verschillende notaties voor dezelfde taal

Specifieke bekwaamheden Logica

a) propositie- en predikatenlogica

  • herkennen welke redeneerproblemen met propositielogica 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 of weerleggen met behulp van natuurlijke deductie
  • bewijzen netjes opschrijven

b) propositielogica

  • voor gegeven beweringen de waarheidstabel opstellen
  • voor gegeven beweringen aangeven of deze tautologisch zijn
  • redeneerfouten herkennen en blootleggen
  • aangeven welke verzamelingen van voegtekens al dan niet functioneel volledig zijn

c) informatica

  • relevante eigenschappen van eenvoudige ingebouwde real-time-systemen en hun onderdelen logisch specificeren
  • de juistheid van logische specificaties aantonen
  • systemen hierarchisch 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 aangeben tussen logische en enkele andere specificatiefformalismen

Onderwerpen

aRealiteit, abstractie, modellen, contracten, verborgen aannames, natuurlijke en formele talen, syntaxis en semantiek, typering, propositie- en predikatenlogica, waarheidstabellen, natuurlijke deductie, specificatie, correctheid van systemen, Chinese dozen (hiërarchische decompositie), proof tools, SQL, eindige automaten, state based systems

Werkvormen

We gaan dit alles oefenen aan de hand van een probleemgeoriënteerd practicum. 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 predikatenlogica. 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 leer je in zelfstudie iedere week nieuwe stof. In responsiecolleges bespreek je je eigen oplossing en die van anderen.

Vereiste voorkennis

Vertrouwd zijn met het verschil tussen een informele en een formele benadering op het niveau van de cursus Formeel Denken, Diskrete Wiskunde of een vergelijkbare cursus. Enige ervaring met modellering. Enige ervaring met een aantal formele (programmeer- en modelleringstalen).

Tentaminering

De cursus bestaat uit een aantal inhoudelijke blokken. Elk blok wordt afgesloten met een schriftelijk deeltentamen. Ook maak je, al dan niet in synergie met R&D, een groot werkstuk. Voor elk schriftelijk tentamen en voor het werkstuk moet je ten minste een 5,5 hebben.

Literatuur

J.F.A.K. van Benthem et al.: Logica voor informatica; Pearson Education Benelux, 2003, ISBN 90-430-0722-6 of een oudere of nieuwere oplage. Dit is verplichte literatuur. 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 gebruiken, het scheelt niet veel.


Evaluatie: studentenquêtes ; geen docentevaluatie bekend Rendement: 85 begonnen, 75 echt meegedaan, geslaagd met 1e kans, geslaagd totaal
Q: