Use and Meaning of Open Terms in Interactive Formal Problem Solving

Computers kunnen nuttige hulp verrichten bij het vinden van een correct bewijs voor een wiskundige stelling, of om te bewijzen dat een computerprogramma voldoet aan zijn specificatie. Dit is het geval, omdat computers snel en efficiënt zijn, grote hoeveelheden informatie betrouwbaar kunnen beheren en - door een geschikte interface - met de menselijke gebruiker kunnen communiceren. Tijdens de constructie van zon bewijs met computerhulp ontstaan uit de aard der zaken onaffe deelbewijzen, of anders gezegd: bewijzen waarin gaten zitten, die later nog exact moeten worden ingevuld. Voor zon bewijs-met-gaten bestaat tot op heden nog geen expliciete theoretische beschrijving, althans vanuit logisch standpunt. Dit geldt evenzeer voor de transformaties die tijdens het bewijsconstructieproces de ene onvolledige toestand in de andere doen overgaan (net zo lang tot het einddoel is bereikt: het complete, verantwoorde en gecontroleerde bewijs). Dit onderzoeksproject legt de theoretische fundering voor dergelijke onvolledige bewijsstructuren en geeft ook een precies verband met hun betekenis, dat wil zeggen een formele uitleg van wat er tijdens het constructieproces precies gebeurt. Daarbij is een theorie ontwikkeld die zo goed mogelijk aansluit bij de praktische toepassingen, zowel bestaande als toekomstige.