Truls Pedersen

Truls Pedersen is working with a project titled "A modal logical framework for social software"  where he uses formal methods (particularly multi-agent modal logic) to analyse social software. Modal logic is an extension of the classical propositional logic which allows modelling of modal aspects of statements, such as "by necessity...", "it is known that...", "through cooperation...".

In this project Truls Pedersen is expressing concepts which are central in social software with  model logic. This allows us to verify properties of social software in the sense that it may reveal what follows from formally specified assumptions, and which properties a formal model may have. In some cases we may also construct algorithms for automatically deciding the validity of  statements about such systems.

The term "social software" may refer computer software where people execute social acts, like  Facebook, Twitter or eBay, or it might refer to procedures which are central for such systems,  like sharing information, negotiating, reaching an agreement, make collective decisions and more.

In this project the term is used in the latter sense, i.e. to describe procedures which are  executed within a collection of autonomous agents. Reasoning about the strategic power of  coalitions of agents (a group of agents which doesn't necessarily make up the entire society) is  one example of application. Agents may choose to cooperate in order to bring about a certain  goal. In a model of such a situation a suitable logic should let us answer questions like "is it  possible to reach the desired goal?", "how many (and who) needs to cooperate in order to reach this goal?" or "which acts/which coalitions do we need to ban if we want to construct a system  where only the majority may force a given situation coming about?".

By modelling these questions in formal logic we can use proof systems which often lend  themselves to automatisation, so that properties of such systems may be verified using a  computer.