Automath
Automath (geautomatiseerde wiskunde) was een formele taal die vanaf 1967 door Nicolaas Govert de Bruijn werd ontwikkeld voor het zodanig uitdrukken van complete wiskundige theorieën dat een erin opgenomen automatische bewijschecker de juistheid van deze theorie kon verifiëren. Het Automath-systeem bevatte vele nieuwe ideeën die later werden overgenomen of opnieuw werden uitgevonden op gebieden zoals de getypeerde lambda-calculus en de expliciete substitutie. Afhankelijke typen zijn een voorbeeld bij uitstek. Automath was ook het eerste praktische systeem dat gebruikmaakte van de Curry-Howard-correspondentie.
Proposities werden weergegeven als verzameling (die in Automath "categorieën" werden genoemd) van hun bewijzen. De vraag of een propositie bewijsbaarheid was, werd een kwestie van het niet-leegzijn van de verzameling (type-inhabitie); de Bruijn was zich niet bewust van Howards werk. Beiden stelden deze correspondentie onafhankelijk van elkaar op.[1] Aangezien Automath op dat moment nooit echt duidelijk in de publiciteit kwam, werd het niet breed toegepast; het bleek echter zeer invloedrijk in de latere ontwikkeling van logische raamwerken en bewijsassistenten.[2][3]
Externe links[bewerken | brontekst bewerken]
- (en) The Automath Archive (mirror)
- (en) Automath door Freek Wiedijk
Bronnen, noten en/of referenties
|