The Method of Variable Splitting

Roger Antonsen
Doktorgradsavhandling, Institutt for informatikk, Universitetet i Oslo, 2008.
@PhdThesis{Antonsen08,
  author =   {Roger Antonsen},
  title =    {The {M}ethod of {V}ariable {S}plitting},
  school =   {University of Oslo},
  year =     2008,
  key =      {Automated Reasoning, Logic, Proof Theory, Connection Method, Tableau Calculus},
  address =  {Department of Informatics},
  month =    {June}
}

Sammendrag

This is a thesis in the intersection of automated reasoning and proof theory. It is in the field of automated reasoning because it is a detailed analysis of certain search space redundancies that, in the end, may lead to more efficient theorem provers. It is in the field of proof theory because formal proofs and properties of such are analyzed in great detail. The thesis is foundational in nature and investigates the fundamentals and the metatheory of a method called variable splitting.

Doktorgradsavhandling

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.