A logic of propositional control for truthful implementations

ABSTRACT

We introduce a logic designed to support reasoning about social choice functions. The logic includes operators to capture strategic ability, and operators to capture agent preferences. We give a correspondence between formulae in the logic and properties of social choice functions, and show that the logic is expressively complete with respect to social choice functions, i.e., that every social choice function can be characterised as a formula of the logic. We show the decidability of the logic and give a complete axiomatization. To demonstrate the value of the logic, we show in particular how it can be applied to the problem of determining whether a social choice function is strategy-proof.

REFERENCES

• 1: C. Areces and B. ten Cate. Hybrid Logics, volume Handbook of Modal Logic, chapter 14, pages 821--868. Elsevier Science Inc., 2006.
• 2: K. J. Arrow, A. K. Sen, and K. Suzumura, editors. Handbook of Social Choice and Welfare, volume 1. Elsevier, 2002.
• 3: E. Bonzon, M.-C. Lagasquie-Schiex, and J. Lang. Efficient coalitions in Boolean games. In K. Apt and R. van Rooij, editors, New Perspectives on Games and Interaction, volume 4 of Texts in Logic and Games, pages 283--297. Amsterdam University Press, 2007.
• 4: B. F. Chellas. Modal Logic: an introduction. Cambridge University Press, 1980.
• 5: P. Dasgupta, P. Hammond, and E. Maskin. The Implementation of Social Choice Rules: Some General Results on Incentive Compatibiliy. Review of Economic Studies, 46: 185--216, 1979.
• 6: A. Gibbard. Manipulation of voting schemes: a general result. Econometrica, 41(4):587--601, 1973.
• 7: H. Moulin. The Strategy of Social Choice. Advanced Textbooks in Economics. North Holland, 1983.
• 8: M. J. Osborne and A. Rubinstein. A Course in Game Theory. The MIT Press, 1994.
• 9: Nicolas Troquard , Wiebe van der Hoek , Michael Wooldridge, A logic of games and propositional control, Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems, May 10-15, 2009, Budapest, Hungary
• 10: Wiebe van der Hoek , Michael Wooldridge, On the logic of cooperation and propositional control, Artificial Intelligence, v.164 n.1-2, p.81-119, May 2005 [doi>10.1016/j.artint.2005.01.003]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Intelligent agents
      I.2.4 Knowledge Representation Formalisms and Methods

General Terms:
Algorithms, Design, Theory