Logic programming for modeling social choice

This page contains a collection of Prolog programs and documents (and some spreadsheets), which are applied to orderings and domain, social decision rules with their possibility theorems, domain conditions, simple games, mechanism design, and so on. I gratefully welcome corrections. Thank you.
updated: 9 Aug 2013

the SCLP toolkit

source codes (Prolog)

These code provides automated (partial) proofs of the classical results in social choice theory. (im)possibility theorems by Arrow(1963); Gibbard-Satterthwaite(1973,1975); Wilson(1972); Sen(1982) by using a basic technique of recursive resolution.And this computational method can be used to find new theorems, especially for investigating (im)possibility results in restricted domains.
Prolog source codes which are cumulatively used.

Introductory manual

None. Please refer my paper in Proc. AESCS-2007 below. And the following papers, especially the first 6 except for the second and the last ones, are self-contained with the Prolog source code.


papers and slides

  • Generating Social Welfare Functions over Restricted Domains for Two Individuals and Three Alternatives Using Prolog. In A. Tavidze (ed.), Progress in Economics Researches, Vol. 18. (downlodable)
  • Modeling a small agent society based on the social choice logic programming, In Proc. of AESCS-2007, pp. 130-140. (The revised paper has been published in "Agent-Based Approaches in Economic and Social Complex Systems V," a title of Springer Series on Agent Based Social Systems.)
  • Proving Arrow's theorem by PROLOG, Computational Economics, Vol. 30, No. 1, pp. 57-63.(Apr/Aug 2007)
  • working papers

  • Programming Social Choice in Logic: Some Basic Experimental Results of Social Choice When Profiles Are Restricted, pdf A version of this paper has been submitted to a journal. October, 2009.
  • Social Choice Logic Programming I, the slide presented at the KGU faculty seminar, October, 2008.
  • The Cube First Method and Profile Sequence Formation in SCLP: Proving classical theorems in social choice theeory . my08c.pdf (pdf, 9 Jul 2008)
  • An automated proof of Arrow's theorem (working paper. 25 Mar 2006) (pdf)
  • an introductory article based on the old version below(html, Japanese): sproof.html (Dec 2006)
  • Generating preference aggregation rules by using PROLOG (working paper, draft: aggr061104.pdf, 11 Nov 2006 Japanese)
  • A Graphical Representation of Arrow's Impossibility Theorem. pdf The Research Bulletin of Economics 34(2), 31 Mar 2009 (Japanese) This is a reproduced image of my research paper, but some footnotes have been added, in the above publication.
  • A logic programming for social choice problems (working paper (Japanese): lpmsc.pdf, 8 Apr 2006)
  • slides on the Cube representation of SWF

  • A graphical representation of Arrow's theorem (a version). graphical_swf.pdf (pdf. 29 Nov 2007)
  • A graphical representation of Arrow's theorem. arrow_theorem.pdf (pdf. 27 Oct 2007; 12 Feb 2007 a minor modification)
  • A cube representation of social welfare function on weak ordering. (now revising) (pdf. 5,8 Feb 2008)
  • A cube representation of social welfare function (linear ordering). cube_swf_1.pdf (pdf. 2,12 Feb 2008)
  • A graphical explanation for a proof of Gibbard-Satterthwaite theorem. GS_theorem.pdf (pdf. 2 Nov 2007)
  • spreadsheet modeling

  • A spreadsheet model of social choice function to analyze the conditions of the Gibbard-Satterthwaite theorem. scf.xls (spreadsheet. 1 Nov 2007) (Japanese)
  • A spreadsheet model of Arrovean social welfare function. swf.xls (spreadsheet. 8 Nov 2007)
  • mechanism design and other social choice related topics


    10 Jan; 18 Mar; 7 May; 11 Jul; 5,19,27 Aug; 22 Nov (2007), 12 Mar; 2-11 May; 8-9 Jul; 8 Aug; 15 Sep (2008); 7 Feb; 23 Mar (2010); 5 Jan (2011).
    &Copyright 2006-2011 Kenryo INDO