Automatisoitu päättely on tekoälyn haara, jonka tavoitteena on tutkia ja kehittää järjestelmiä, jotka tuottavat eksakteja ratkaisuja tietyllä rajoitekielellä kuvattuun ongelmaan. Tällaisten järjestelmien sovellukset pohjautuvat deklaratiiviseen lähestymistapaan, jossa alkuperäisen ongelman eksponentiaalinen hakuavaruus esitetään implisiittisesti loogisten tai matemaattisten rajoitteiden avulla. Tämän lähestymistavan ansiosta yhdellä järjestelmällä voidaan ratkaista monia erilaisia laskennallisesti vaikeita ongelmia.
Modernit logiikkapohjaiset järjestelmät pystyvät myös tuottamaan todistuksia siitä, että ratkaisua ei löydy. Tämä ominaisuus on huomattavan tärkeä sellaisissa sovelluskohteissa, joissa oikeellisuudesta ei voida tinkiä, kuten laitteistojen sekä ohjelmistojen verifioinnissa. Rajoiteoptimointi taas kattaa deklaratiivisen lähestymistavan kautta tilanteita, joissa halutaan löytää tietyssä mielessä paras mahdollinen ratkaisu. Sovelluskohteissa voidaan tällöin esimerkiksi säästää resursseja mahdollisimman tehokkaasti.
Vuodesta 2022 alkaen olen työskennellyt tutkijatohtorina Suomen Akatemian rahoittamassa projektissa Helsingin yliopiston tietojenkäsittelytieteen osastolla. Tutkimukseni keskittyy erityisesti inkrementaalisten logiikkapohjaisten päättely- sekä optimointimenetelmien kehittämiseen laskennallisesti vaativien ongelmien ratkaisemiseksi. Sovelluskohteina tutkin parhaillaan muun muassa sosiaalisesta valinnasta, formaalista argumentaatiosta sekä loogisesta epäkonsistenssista kumpuavia ongelmia.