Disputas: Roger Antonsen

Prøveforelesning

Bedømmelseskomité

Professor Matthias Baaz, Institute of Discrete Mathematics and Geometry, Vienna University of Technology, Østerrike
Professor Wolfgang Bibel, Darmstadt University of Technology, Tyskland
Researcher Martin Giese, Institutt for informatikk, Universitetet i Oslo

Leder av disputas:  Arne Maus

Veileder:  Professor Arild Waaler (UiO), professor Reiner Hähnle (Chalmers University of Technolgy)

Sammendrag

I sin avhandling, utført ved Institutt for informatikk ved Universitetet i Oslo, har Roger Antonsen dannet det teoretiske grunnlaget for en metode som potensielt kan innebære en forbedring og effektivisering av automatisk resonnering og bevissøk.

Studiet av hvordan man kan få maskiner til å tenke eller resonnere har blomstret opp sammen med utviklingen av datamaskiner og informasjonsteknologi. Området, som kalles automatisk resonnering, har mange anvendelsesområder. Ved hjelp av symbolske verktøy kan man representere og behandle kunnskap og slik lage dataprogrammer som, for eksempel, bistår mennesker i komplekse beslutningsprosesser eller søker etter formelle bevis for påstander og teoremer innenfor matematikk. Det handler om å få datamaskiner til å kunne regne seg frem til konklusjoner fra gitte premisser eller å kunne utlede ny kunnskap fra allerede gitte data. Dette er som regel svært komplekst og krever presise og effektive søkemekanismer.

Antonsens avhandling befinner seg i skjæringspunktet mellom matematisk logikk, automatisk resonnering og bevisteori, og grenser til områder som kunstig intelligens, beslutningsteori, kunnskapsrepresentasjon og kompleksitetsteori. Den definerer et matematisk verktøy som kan brukes til å identifisere og fjerne spesifikke overflødigheter i logiske kalkyler som brukes til automatisk resonnering. Metoden, som er basert på en detaljert analyse av avhengighetsforholdet mellom universelle uttrykk ("for alle"-formler) og forgrenende uttrykk ("eller"-formler), danner grunnlaget for en effektivisering av automatiske søkemekanismer. I sin avhandling tar Antonsen for seg en rekke forskjellige logiske systemer og ser på hvordan metoden kan anvendes på disse. Gjennom nye matematiske resultater påvises det blant annet hvordan metoden kan gi opphav til eksponensielle forbedringer i automatiske søk.

Kontaktperson

For mer informasjon, kontakt Lena Korsnes.