Beweren en bewijzen/de zuilen/Zekerheid/7. Bewijsassistenten

Uit Werkplaats
Ga naar: navigatie, zoeken
de opzet 2017-18    KalenderIcon.gif multimedia kwaliteit commentaren
site map


Beweren en bewijzen
Wijsheid omgaan met onzekerheid: met open blik op wankele ondergrond levenspad bewandelen
Vernuft aanpak van glibberige problemen precies redeneren op het hoogste niveau
vier zuilen → Artefacten Formalisering Taal Zekerheid
1. Rationaliteit Rationaliteitsvierkant 4 werelden Beweren is moeilijk Overtuigen
2. Modellen Focus Precisie Logica Stelling en bewijs
3. Model en realiteit Specificaties Domeinmodel Syntax en semantiek Waarheid
4. Correctheid Structuur Correctheidsstelling Typering Nagaan
5. Methoden Decompositie Systemat. vertalen Definities Natuurl. deductie
6. Theorie Domeintheorie Tijd Tijdslogica Wiskunde
7. Complexiteit Hiërarch. decompositie Vereenvoudigingen Modules Bewijsassistenten
8. Generalisering Standaardisatie Parametrisatie Talen Hulpstellingen
Beweren en bewijzen/de zuilen/Zekerheid/7. Bewijsassistenten

Aan deze pagina wordt nog gewerkt. Bedankt voor uw begrip.

literatuur

...

Voor het echte, professionele werk worden thans allerlei geavanceerde bewijsassistenten ontwikkeld die meer kunnen dan alleen toezien op het correct toepassen van de deductieregels. Over een paar jaar zal het niet meer weg te denken zijn dat informatici een belangrijk deel van hun werk met zulke bewijsassistenten verrichten. Hun gebruik zal vergelijkbaar moeizaam te leren zijn dan het professionele gebruik van bijvoorbeeld Photoshop of een commercieel CAD-programma. Sommige informatici zullen later ook zelf onderzoek doen omtrent de grondslagen en de ontwikkeling van zulke gereedschappen. Informatiekundigen zullen daarom naar verwachting minder vaak zulke gereedschappen gebruiken, maar ze moeten wel hun mogelijkheden en beperkingen heel goed kennen.

In deze cursus gaat het niet om geavanceerd gebruik van een geavanceerd stuk professioneel gereedschap maar om de basis: wat moet iedereen eens met zo'n bewijsassistent gedaan hebben om later in te kunnen schatten waar zoiets van pas kan komen en wat het inhoudt.