In dit proefschrift wordt gekeken naar wiskundige stellingbewijzers (theorem provers). Dit zijn computerprogramma's die een wiskundig document kunnen controleren op fouten en ongerijmdheden. Vaak bieden ze een auteur ook mogelijkheden om zo'n document tot stand te laten komen.
Alle wiskundige stellingbewijzers zijn gebaseerd op een of andere logische taal. Het is noodzakelijk dat de te controleren wiskunde is geformaliseerd in zo'n logische taal. Omdat de computer de inventiviteit van een menselijk wiskundige mist, moeten de documenten uitgespeld worden tot in de fijnste details. De computer beschikt echter over een aantal eigenschappen die hem uiterst geschikt maken voor zijn verificatietaak: Hij is precies, onvermoeibaar, snel, betrouwbaar en klaagt niet.
In dit proefschrift wordt voor de logische taal de zogenaamde typentheorie gebruikt. Informele wiskundedocumenten worden direct gecodeerd in typentheorie, inclusief de redeneringen in de bewijzen. Wiskunde, gecodeerd in typentheorie, die gecontroleerd is door de computer is volledig correct, mits het verificatieprogramma correct is. Gelukkig kan de kern van zo'n programma relatief klein blijven, zodat handmatige controle van de correctheid mogelijk is. Men zegt wel dat typentheoretische stellingbewijzers voldoen aan het De Bruijn criterium.
Het formaliseren van informele wiskunde blijkt nog niet zo makkelijk te zijn. Er moeten veel details gegeven worden, waardoor vooral formele bewijzen erg groot kunnen worden. Vaak gaat het om grote aantallen relatief triviale stappen. Bovendien moeten er tijdens het formaliseren allerlei implementatiekeuzes gemaakt worden die grote gevolgen kunnen hebben voor de structuur van het document. Verder is er een groot aantal onopgeloste problemen op het gebied van het hergebruik van en communicatie met geformaliseerde wiskunde tussen stellingbewijzers en andere computerwiskundesystemen.
Het proefschrift richt zich op de volgende drie problemen: het automatisch bewijzen van tautologieën door middel van berekeningen binnen bewijzen, de interactieve presentatie van wiskundige documenten nadat ze geformaliseerd zijn, en de communicatie tussen stellingbewijzers en andere computerwiskundesystemen zoals bijvoorbeeld computeralgebrasystemen. Daartoe zijn de volgende hoofdstukken opgenomen in het proefschrift.
Hoofdstuk 2 behandelt de theorie achter stellingbewijzers. Specifieker wordt de Calculus of Inductive Constructions behandeld. Dit is de typentheorie die in de populaire Coq stellingbewijzer gebruikt wordt. Dit hoofdstuk toont aan dat veel wiskundige begrippen elegant gecodeerd kunnen worden in de Calculus of Inductive Constructions. Het hoofdstuk maakt het proefschrift ``self-contained'' en legt een basis voor de andere hoofdstukken.
Hoofdstuk 3 richt zich op berekeningen binnen bewijzen. Hoewel het doen van (symbolische) berekeningen tot de hoofdactiviteiten van een wiskundige behoort, maken berekeningen geen deel uit van een in typentheorie gecodeerde logische redenatie. In dit hoofdstuk wordt dit gegeven gebruikt om triviale redeneerstappen te automatiseren door middel van een principe dat reflectie genoemd wordt. Via een aantal case studies wordt gedemonstreerd hoe dit principe werkt en wat de grenzen zijn.
Hoofdstuk 4 gaat over interactieve presentatie van formele wiskundige documenten. Het gaat hierbij om interactieve presentatie gebaseerd op inhoudelijke typentheoretische structuur, waarbij de wiskunde gepresenteerd wordt in de wiskundige omgangstaal. Het wordt de lezer bijvoorbeeld mogelijk gemaakt om het niveau van detail waarop bewijzen gepresenteerd worden, dynamisch te veranderen. Aan de hand van een door ons geïmplementeerd prototype tool laten we zien hoe wiskundige inhoud gecodeerd in typentheorie in principe op een natuurlijke en interactieve wijze gepresenteerd kan worden.
Hoofdstuk 5 behandelt de communicatie van stellingbewijzers met computeralgebrasystemen. Het gaat hierbij om communicatie gebaseerd op open standaarden zoals de OpenMath taal. Computeralgebrasystemen excelleren in het doen van symbolische berekeningen, maar missen de garantie voor correctheid die stellingbewijzers bezitten. In een concreet voorbeeld worden formele bewijzen van primaliteit van grote getallen gegenereerd, hetgeen meer rekenkracht vereist dan aanwezig bij de stellingbewijzer. Daarom wordt de hulp ingeroepen van een computeralgebrasysteem. Dit voorbeeld toont aan dat communicatie tussen computerwiskundesystemen nuttig en mogelijk is.
Hoofdstukken 1 en 6 bevatten de inleiding respectievelijk de conclusies van het proefschrift. Deze hoofdstukken plaatsen de bevindingen uit de andere hoofdstukken in de context van een algemene zoektocht naar het ideale computerwiskundesysteem dat ondersteuning biedt bij alle aspecten van het wiskundige werk.
|
thesis2001.pdf.gz: | The manuscript as gzipped PDF. |
 |
Reflection in Coq: Some files related to Chapter 3. |
|
Interactive Mathematical Documents: Some files related to Chapter 4. |
|
Pocklington's criterion: Some files related to Chapter 5. |
|
Stellingen behorende bij het proefschrift (in Dutch) |
|
Photos of the defence ceremony |