Objecten met onbekende delen in stellingbewijzers

30 maart 2004

NWO-promovendus Georgi Jojgov heeft tijdens zijn promotie-onderzoek aan de Technische Universiteit Eindhoven een model gemaakt van een bewijsassistent. Dit model bestudeert de theoretische aspecten van het maken van bewijzen in interactie met een computer.

Een interactieve bewijsassistent (ook wel stellingbewijzer genoemd) is een computerprogramma waarmee wiskundigen en informatici theorieën en bewijzen ontwikkelen. Het maken van zulke bewijzen gaat meestal stap voor stap vanwege de hoge complexiteit van de theorieën die worden gebruikt. Daarom moet een bewijsassistent in staat zijn om met zogeheten incomplete objecten om te gaan. Een incompleet object is er een waar een aantal delen van onbekend zijn. Bijvoorbeeld ?2+1 is een incompleet object waarin '?' een onbekende is. Hoewel we niet weten waar de '?' voor staat, we kunnen er mee omgaan. Wij kunnen er formules mee opbouwen, mee rekenen en we kunnen er stellingen over bewijzen (bijvoorbeeld ?2+1>0).

Zulke onbekende waarden gedragen zich als variabelen, maar wel op het metaniveau. Het zijn namelijk variabelen waarvoor een waarde wordt gezocht, interactief met een computer. Ze worden ook metavariabelen genoemd en je kom ze ook tegen als je bewijzen gaat maken. Daar staan ze voor incomplete bewijzen, oftewel bewijzen waarin sommige onderdelen nog niet bewezen zijn. De promovendus laat zien dat een nieuw soort metavariabele nodig is om niet-afgemaakte bewijzen op een computer te kunnen representeren. De reden hiervoor is dat een incompleet bewijs zelf kan afhangen van incomplete objecten. Om dit precies te maken, introduceert de promovendus bindende metavariabelen die het mogelijk maken om een gebonden variabele te gebruiken voordat haar binder is gemaakt.

De promovendus definieerde ook een taal en regels, waarmee bewijzen kunnen worden gemaakt. De termen van deze taal heten tactieken en kunnen gezien worden als voorgebakken recepten om bewijzen in specifieke gevallen te maken. Een voorbeeld van tactiek is een beslissingsprocedure voor propositie logica. De onderzoeker stelde een aantal regels op waamee uitgerekend kan worden wat de uitkomst is van de toepassing van een tactiek op een bepaald doel, en onderzocht sommige eigenschappen daarvan.

Het onderzoek naar methoden om interactief met de computer bewijzen te construeren is onderdeel van het onderzoek naar computerondersteunende verficatie. Hierbij probeert men met behulp van computergereedschappen eigenschappen van systemen te verifieren. Vaak gaat het daarbij om computersystemen die men probeert zo foutloos mogelijk te krijgen.

Meer informatie bij

  • Georgi Jojgov (TUE, Wiskunde en Informatica, Georgi spreekt Engels)
  • t: +31 (0)40 247 5004, g.i.jojgov@tue.nl
  • Promotie 5 april, promotoren prof. dr. J.C.M. Baeten en prof. dr. H.P. Barendregt (KUN)