Logic for Automated Mechanism Design and Analysis

Abstract

Recent years have witnessed an explosion of interest in the issues surrounding the use of social choice mechanisms and economic resource allocation mechanisms in settings where the participants are computer programs. Algorithmic mechanism design, and the recent emergence of computational social choice theory are two examples of this growth of interest. If we take seriously the idea that computational agents will participate in economically inspired mechanisms, then it is natural to consider the questions of knowledge representation and reasoning for them. In this talk, we describe our work in this area, particularly as it relates to the specification and verification of social choice mechanisms, and coordination mechanisms such as social laws. We motivate and introduce the main research issues in the area, discussing, for example, the succinct representation of social choice rules, the complexity of reasoning with such representations, and the handling of preferences. We conclude by showing discussing the relationship of our work to mechanism design as it is understood in economics. The talk will report joint work with Thomas Agotnes (Bergen), Wiebe van der Hoek (Liverpool), Marc Pauly (Stanford), and Paul E. Dunne (Liverpool).