26 januari 2001
Sequents and link graphs. Contraction critera for refinements of
multiplicative linear logic.
Drs. G-W.Q. Puite, Wiskunde en Informatica 10:30 uur
Promotor: Prof.dr. I. Moerdijk, co-promotor: Dr. H.A.J.M. Schellinx
In dit proefschrift beschouwt wiskundige Quintijn Puite subsystemen
van lineaire logica (Girard, 1987), die niet alleen een logische
status toekennen aan het aantal voorkomens van een formule, maar
ook onderscheid maken in de onderlinge samenhang van de formules,
bijvoorbeeld hun volgorde. Zo'n gestructureerde verzameling van
formules, die we een sequent noemen, is geldig precies dan als zij
afleidbaar is. Bij een eventuele afleiding hoort een zogenaamd
bewijsnet: een spoorwegkaartachtig diagram bestaande uit linken (of
knopen), verbonden door lijnstukken. Om een sequent te onderzoeken
op geldigheid, kunnen we nu elk van zijn kandidaat-bewijsnetten
onderwerpen aan een samentrekbaarheidstest, die aangeeft of het
daadwerkelijk een bewijsnet is. Genoemde samentrekking is
gedefinieerd op de ruimte van linkgrafen, die zowel de
kandidaat-bewijsnetten als de sequenten omvat. Puite's aanpak
verschilt in zoverre van de gebruikelijke theorie dat hij
hypothesen toestaat en een algemenere definitie van link hanteert,
wat de theorie in vele opzichten geschikter maakt. Het onderzoek,
onderdeel van de zuivere bewijstheorie, is tevens de formele basis
van toepassingen in de linguïstiek en de informatica, bijvoorbeeld
voor automatische zinsontleding.