Brontekst bekijken van Beweren en bewijzen/de aanpak/vier zuilen

<noinclude>{{BenB/Inhoud|Stof en volgorde van deze cursus|}}[[Categorie:Public]]</noinclude>
{{BenB/inleiding|kweeste=
{{:Glossarium/wijs}}

Expert worden op het gebied van onzekerheid - deze cursus zal daarbij helpen.  
|literatuur=

{{pencast|H. Wupper: Tempelbau (in het Duits)|2=http://www.livescribe.com/cgi-bin/WebObjects/LDApp.woa/wa/MLSOverviewPage?sid=GzRn5NHhfvcl}}
}}

Onzekerheid is griezelig. Maar men kan leren, zelf zekerheid in zijn hoofd te  scheppen. Men kan leren een griezelig probleem - lang voor men een oplossing  ziet - in deelproblemen op te splitsen, die elk voor zich al stukken minder griezelig zijn. Men kan leren exacte en ondubbelzinnige beweringen te formuleren waarmee  het wezenlijke van het onwezenlijke wordt gescheiden. Men kan dingen bewijzen  en dan goed nagaan wat men eigenlijk bewezen heeft en wat dat zegt. Kortom:  men kan leren, macht over de onzekerheid te krijgen: door middel  van scherp redeneren op het hoogste niveau, door middel van logica en wiskunde.

<big>Maar hoe? </big>Onze leerdoelen verbinden dit redeneren op het hoogste niveau met het vraagstuk van correctheid van gemaakte dingen.


{| class="wikitable" align="center"
! colspan="4" | Vier inhoudelijk orthogonale cursussen die ook los van elkaar gevolgd zouden kunnen worden:
|-
! Artefacten !! Formalisering !! Taal !! Zekerheid
|-
| {{:Beweren en bewijzen/de zuilen/Artefacten}}
| {{:Beweren en bewijzen/de zuilen/Formalisering}}
| {{:Beweren en bewijzen/de zuilen/Taal}}
| {{:Beweren en bewijzen/de zuilen/Zekerheid}}<onlyinclude>
|-
! colspan="4" | Na voltooiing van deze cursus kun je...
|-
|
* een gegeven of nog te bedenken artefact systematisch hi&euml;rarchisch onderverdelen,
* beredeneren dat bepaalde eigenschappen van het artefact waar gemaakt worden door de eigenschappen van zijn gezamenlijke onderdelen,
* idealiter gewenste eigenschappen op een verantwoorde manier afzwakken tot eigenschappen die realiter waar gemaakt kunnen worden,
* aangeven wat de rol van formalismen en formele methoden in dit proces is,
* een exemplarische formele methode en de bijbehorende bewijsassistent (in casu Coq) ervoor gebruiken,
* een verslag over de correctheid van het artefact maken waarin de resultaten van formele methoden voor leken toegankelijk gepresenteerd worden.
|
* uit een vaag en niet afgebakend reëel probleem (in casu een correctheidsvraagstuk over een artefact) een deelprobleem destilleren dat zich formeel bewijzen laat,
* een fragment  van de realiteit onder een relevant aspect formeel modelleren (in casu m.b.v. propositie- en predicaatlogica),
* verantwoorden dat het model werkelijk slaat op de fysieke realiteit,
* met behulp van een exemplarische formele methode en de bijbehorende bewijsassistent (in casu Coq) een volledig bewijs leveren,
* aangeven wat de valkuilen zijn bij het toepassen van formele methoden op vage problemen uit de realiteit en hoe men daarmee systematisch omgaat.
|
* een exemplarische specificatie- en een verificatietaal (in casu Coq en natuurlijke deductie) toepassen op middelgrote correctheidsvraagstukken,
* conform een formele grammatica de syntaxboom van teksten uit een formele taal construeren
* en langs deze boom de betekenis van de tekst afleiden,
* middelgrote specificaties correct in deze taal opschrijven
* en wel zo dat ze ook voor mensen leesbaar en begrijpelijk zijn,
* een bewijsassistent (in casu Coq) gebruiken voor correctheidsbewijzen.
|
* beweringen opschrijven in propositie- en predicaatlogica,
* vraagstukken als stellingen met aannames en conclusies formuleren in logica,
* stellingen op een gestructureerde manier in natuurlijke taal bewijzen,
* in het geval van propositielogica: waarheid aantonen m.b.v.
** waarheidstabellen en
** semantische tableaus,
* stellingen bewijzen met natuurlijke deductie
** met potlood en papier en
** met behulp van een bewijsassistent (in casu Coq).</onlyinclude>

|-
!colspan="4" align="center" | Een filosofisch verantwoord verhaal met oplopende complexiteit:
|-
|colspan="4" align="center" | 
{| class="wikitable"
|-
! width="150"|{{BenB/laag|1|Rationaliteit}}
| {{:Beweren en bewijzen/het verhaal/1. Rationaliteit}}
|-
! {{BenB/laag|2|Modellen}} 
| {{:Beweren en bewijzen/het verhaal/2. Modellen}}
|-
! {{BenB/laag|3|Model en realiteit}}
| {{:Beweren en bewijzen/het verhaal/3. Model en realiteit}}
|-
! {{BenB/laag|4|Correctheid}}
| {{:Beweren en bewijzen/het verhaal/4. Correctheid}}
|-
!  {{BenB/laag|5|Methoden}}
| {{:Beweren en bewijzen/het verhaal/5. Methoden}}
|-
!  {{BenB/laag|6|Theorie}}
| {{:Beweren en bewijzen/het verhaal/6. Theorie}}
|-
! {{BenB/laag|7|Complexiteit}}
| {{:Beweren en bewijzen/het verhaal/7. Complexiteit}}
|-
! {{BenB/laag|8|Generalisering}}
| {{:Beweren en bewijzen/het verhaal/8. Generalisering}}
|}
|-
!colspan="4" align="center"| Het Cartesisch product: vier parallelle cursussen in één:
|-
|colspan="4" align="center"|
[[Afbeelding:Benb-4zuilen.png|center]]
{{BenB/Inhoud||}}
|}

De docenten willen jullie helpen experts te worden op het gebied van onzekerheid. Maar dat kun je alleen leren als je ook af en toe aan onzekerheid bloot staat. Bijvoorbeeld door practicumopdrachten uit te voeren waarvan niemand al in het begin de goede  oplossing kent. Als je dat niet gewend bent, is dat griezelig, dat weten we.  Maar nu is de tijd, eraan gewend te raken. 

<big>Waarheen? </big>Als je deze cursus voltooid hebt, heb je twee proeven van bekwaamheid geleverd:
; Werkstuk : Je hebt samen met een paar medestudenten een werkstuk geschreven waarin je laat zien dat je op professioneel niveau iets kunt doen dat tot de kern van de informatica en informatiekunde hoort.
; Theorie : Je hebt in een aantal tentamens aangetoond dat je de nodige theoretische kennis hebt en kunt toepassen. Deze tentamens doe je in een bepaalde volgorde, volgens een bepaald rooster. Elk tentamen is de afsluiting van één van de hoofdstukken waarin de stof onderverdeeld is.

Hoe het allemaal in zijn werk gaat staat beschreven in [[Beweren en bewijzen/de opzet|de opzet]].