Disputas: André Rognes

Cand.scient. André Rognes vil forsvare sin avhandling for graden dr.philos.:

On the methods of mechanical non-theorems

André Rognes

Tid og sted for prøveforelesninger

Bedømmelseskomité

  • Professor Erich Grädel, RWTH Aachen University

  • Professor Elvira Mayordomo Cámera, Universidad de Zaragoza

  • Professor Dag Normann, University of Oslo

Leder av disputas

Instituttleder Arne Huseby, Matematisk institutt, Universitet i Oslo

Sammendrag

I avhandlingen beskrives en ny oppdeling av Hilberts Entscheidungsproblem. Oppdelingen er basert på en familie av mekaniske prosedyrer, som hver er istand til å liste opp sin del. Noen av disse prosedyrene er kjørt på alminnelige datamaskiner og har løst instanser av Entscheidungsproblemet som ligger utenfor rekkevidde for tidligere implementasjoner.

Instanser av Entscheidungsproblemet kan vi tenke på som likninger hvor de ukjente løper over relasjoner. Vi søker å fremstille prosedyrer for å svare på om slike likninger har en løsning eller ikke. Likningene som tidligere har ligget utenfor rekkevidde er kjennetegnet ved at de utelukkende har løsninger over uendelige mengder.

For å få svar på spørsmål om eksistens av relasjoner over mengder som nødvendigvis er uendelige, leter prosedyrene etter løsninger på likninger i endelige, men abstrakte, algebraer av relasjoner. Sammen med et tensorprodukt for algebraer av relasjoner gir dette en strikt generalisering av prosedyren kjent som endelig modell-søk.

I første tredjedel av avhandlingen innføres en ny variant av relasjons-algebraer. Disse har den egenskapen at det til hver løsbare likning finnes en endelig algebra hvor likningen har en løsning. Med hensyn på å representere løsninger i mekaniske prosedyrer, er egenskapen en forbedring av Löwenheim-Skolem teoremet, som sier at det til hver løsbare likning finnes løsninger over tellbare mengder.

For å kunne bruke en abstrakt algebra til a svare på om en likning er løsbar, må algebraen være representabel. De to resterende tredjedelene av avhandlingen handler om hvordan man kan bruke endelige tilstands-maskiner til å definere, og dermed regne ut, basiser til algebraer som nødvendigvis er representable. Dette uten å regne ut hele algebraen som typisk er for stor til å få plass i en bok eller datamaskin.

For mer informasjon

Kontakt Matematisk institutt.

Publisert 6. juni 2013 16:18 - Sist endret 19. juni 2013 09:08