Op weg naar een automatisch wiskundige

10-05-2021

11.45

Online

Superposition for Higher-Order Logic

A. Bentkamp

prof.dr. W.J. Fokkink, dr. J.C. Blanchette, dr. U. Waldmann

Faculteit der Bètawetenschappen

Exacte wetenschappen

Promotie

Onderzoekers werken al jaren aan computerprogramma’s die zelf wiskundige bewijzen kunnen vinden, zogeheten stellingbewijzers. Het proefschrift van onderzoeker Alexander Bentkamp draagt daar op een bijzondere manier aan bij, door twee takken van onderzoek die tot nu toe altijd gescheiden waren, samen te voegen.

De zoektocht naar automatische wiskundigen was voorheen verdeeld in stellingbewijzers voor eerste-orde logica en stellingbewijzers voor hogere-orde logica. Eerste-orde logica is de simpelste van de twee. De eenvoud ervan stelde onderzoekers in staat een efficiënte stellingbewijzer te ontwikkelen. Een van de succesvolste technieken die aan deze stellingbewijzer ten grondslag ligt, en die in de jaren negentig is ontwikkeld, heet superpositie.

Hogere-orde logica is een meer expressieve en complexe logica. De complexiteit ervan heeft onderzoekers er lang van weerhouden een superpositie-achtige techniek voor deze logica te ontwikkelen. In plaats daarvan zijn andere technieken voor hogere-orde logica ontstaan.

Het promotieonderzoek van Bentkamp brengt deze werelden samen. Hij heeft samen met zijn collega’s de superpositie aangepast aan hogere-orde logica en er een stellingbewijzer op geprogrammeerd. Deze stellingbewijzer won de categorie "hogere-orde logica" in de stellingbewijzer-wedstrijd 2020.

In een theoretisch gedeelte hebben de onderzoekers technieken ontwikkeld om ervoor te zorgen dat de zoekruimte volledig wordt doorzocht zonder enig mogelijk bewijs over het hoofd te zien. In een praktisch gedeelte hebben zij de techniek geprogrammeerd en geëvalueerd.

Het is onwaarschijnlijk dat computers menselijke wiskundigen gaan vervangen. Dat neemt niet weg dat stellingbewijzers nuttige hulpmiddelen aan het worden zijn in het wiskundig onderzoek. Ze zijn niet alleen interessant voor wiskundigen; ook computerwetenschappers en softwareontwikkelaars kunnen hier profijt van hebben. Zij kunnen stellingbewijzers bijvoorbeeld inzetten om te bewijzen dat software veilig is en correct werkt.

Meer informatie over het proefschrift

Livestream: https://www.youtube.com/channel/UCnN8TaVYe83472ewz9CH9HA