Tämän projektin aiheena on automatisoidun päättelyn taustateoria. Jo 1930-luvulla osoitettiin, että matematiikkaa ei voi täysin automatisoida millään menetelmällä, ja tämän jälkeen matemaatikot ja loogikot ovat pyrkineet löytämään sopivasti rajoitettuja systeemejä joissa päättely voidaan kuin voidaankin automatisoida. Tämä projekti on osa kyseisen aihealueen modernia tutkimusta. Tavoitteeja on löytää eri systeemejä (eli logiikoita) erilaisiin automatisoituviin päättelytehtäviin. Mitä ilmaisuvoimaisempi logiikka, sitä hitaampaa on sen avulla suoritettava päättely. Ilmaisuvoiman ja käyttönopeuden välillä on siis käänteinen suhde. Projektin tavoitteena on rakentaa yhtenäinen taustateoria automatisoituvien logiikoiden teoriaa varten. Tällaisen taustateorian avulla eri logiikoiden heikkouksia ja vahvuuksia voidaan entistä paremmin tutkia ja ymmärtää.

2019

2024