Hjem
Click

Institutt for informasjons- og medievitenskap

Truls Pedersen

I dette prosjektet anvender vi formelle metoder (særlig multiagent modallogikk) for å analysere sosial programvare. Vi uttrykker begreper som er sentrale i sosial programvare i modallogikk. Dette tillater oss å verifisere egenskaper ved sosial programmvare. Vi ønsker å konstruere algoritmer for automatisk avgjørelse av gyldigheten av påstander om slike systemer.

Begrepet "sosial programvare" kan referere både til dataprogrammer hvor mennesker utfører sosiale handlinger, som for eksempel Facebook, Twitter og eBay, og også til prosedyrene som er sentrale for slike  programmer: dele informasjon, forhandle, komme til enighet, slutte felles avgjørelser og mer.

Vi bruker begrepet sosial programvare for å beskrive prosedyrer som utføres i en samling av autonome agenter. Preferanseaggregering er et eksempel på slike prosedyrer. Her studeres prosedyrer som forsøker å finne en felles preferanseprofil for et samfunn basert på individenes preferanser. Et velkjent resultat for preferanseaggregering er Arrows umulighets teorem. Dette teoremet, og andre egenskaper ved sosiale prosedyrer, bevises ofte ved hjelp av spillteori. Ved å formulere slike problemstillinger i formal logikk kan vi benytte bevissystemer som ofte lar seg automatisere, det vil si at egenskaper ved slike prosedyrer kan verifiseres ved hjelp av en datamaskin.