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); GibbardSatterthwaite(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.
 preference generator (gprf06,
revised 26 Dec 2006, 7 Jan 2007;30 Oct 2007; 2 & 7 May 2008)
The recent revision includes modeling of consistent relations and a new signbased representation regarding cyclic relation.
 automated proofs for the Arrow's SWF and its variants
(cswf06, original (revised 24 Dec 2006, 5 Jul 2007)
(cswf07, weak ordering (revised 29 Oct 2007)
(cswf08, May's conditions, new binary tables for SWF, and faster recursive proving method (revised 9 Aug 2013; 11 May & 15 Sep 2008)
Revised!

Errata
I'm sorry for bugs in eariler versions. IIA and some axioms were too loose so that it could not reproduce
the Arrowtype result for weak ordering (fixed in cswf07).
Bug fix for dictatorship and rewrite for several Pareto conditions (fixed in cswf08).
 automated proofs for the GibbardSatterthwaite's SCF (spsc06, revised 26 Dec 2006; 3 Sep 2009)
Pareto condition is corrected.
 common admissible domain and decomposability (KalaiMuller theorem)
(
dcdi06, revised 6 Jan 2007)
 common (or individual) admissible domains: singlepeakedness, value restriction, cyclical dependence and so on.
(
drsc06, 26 Dec 2006; revised 6 Jan 2007)
 dual simple games, essential decomposability, and transitive
dominace: Theorems by Shapley(1962), BlairMuller(1983), and Kaneko(1975)
(sged06, 31 Dec 2006; revised 10 Jan 2007)
 swing, pivotality, dominance relation, and core of simple game.
(power, 6 May 2007)

a rule miner: automated discovery for the theorems on simple games
(rminer.pl 11 Jul 2007)
 distances of Dodgeson and Kemeny.Dodgeson and Kemeny.
( metric_d.pl and
metric_k.pl and
metric_rm.pl Aug 2007; revised 2 May 2008)
 references(text file):
cref.pl (19 Jan 2007; 7 May 2008)
 common programs:
menu.pl (stopwatch/2, tell_goal/[2,3])
Introductory manual
None. Please refer my paper in Proc. AESCS2007 below.
And the following papers, especially the first 6 except for the second and the last ones, are selfcontained with the Prolog source code.
Paper
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 AESCS2007, pp. 130140. (The revised paper has been published in
"AgentBased 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. 5763.(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 GibbardSatterthwaite theorem.
GS_theorem.pdf (pdf. 2 Nov 2007)
spreadsheet modeling
A spreadsheet model of social choice function to
analyze the conditions of the GibbardSatterthwaite 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
Other experimental results and alternative modeling

Automated design of Arrovian social welfare function: the 2 x 3 case of
general possibility theorem
(swf.pl, Prolog, 7 Feb 2006)

Analyzing proof process of the general possibility theorem :
dictatorship, decisiveness, and pivotality
(swf_d.pl, Prolog, 6 Mar 2006)
 Simulating the original proof of Arrow (1952)
(Prolog source code): arrow52.pl, 15 Mar 2010)

 domain restriction, simple games, effectivity function, and stability of the core
(Prolog source code): sp06d.pl, 10 Nov 2006)
 A logic programming for social choice problems with
analysis of majority vote and maximal acyclic sets
(Prolog source code): sproof_f.pl, 20 Jun 2006)

Automated design of strategicproof social choice function
(sproof.pl, Prolog, 13 Jan 2006)
 Voting and social choice rules: simple majority vote, Borda rule, pirwise majority, and
Masuzawa rule. The example is cited from the book of social choice theory by
Y. Saeki(1980). (v) (Prolog, 25 Jan 2004)
 A sequential voting example in Dixit and Nalebuff(1991). (v) (Prolog, 9 Jan 2006)

Analyzing majority votes and the acyclic sets with the
expanded versions of automated proof of the impossibility theorems
(v) (sproof_f.pl, Prolog, 20 Jun 2006)

Automated design of strategicproof social choice function
(v) (sproof.pl, Prolog, 13 Jan 2006)
2person and 3alternative case of the GibbardSatterthwaite theorem.
Generating SPobeying SCFs by means of recursive construction with
MM (Maskinmonotonicity) condition started with a Pareto efficient
preference profile which can be seen as an automated proof for the
theorem.

Automated design of Arrovian social welfare function: the 2 x 3 case of
general possibility theorem
(v) (swf.pl, Prolog, 7 Feb 2006)
2person and 3alternative case of the Arrow's impossibility theorem.
A worksheet which analyzes the experimental data by using
swf_b.pl with some additional codes:
swf_b.xls(
=>swf_a.zip 416KB)
(Added: 6 Mar 2006)
An output of the extended version of binary relation based remodeling
of swf.pl (swf_d.txt) where the agent 2
who has privileged to decide the SWF on the pair (b,c) locally at
profile (1,2) will grow decisive, indeed proved to be a dictator truely.
Additionally, some code of displayingswf command in swd_d.pl
((source code))
and figures which show the patterns of IIAequivalent profiles
(iia_profiles.txt).
 Simulation of Nash implementation under abstract social choice environment (20012002,2005)
The prolog program which generates the possible SCC(social choice correspondings)
and verifies several prerequisite conditions for Nash implementability (such as Maskin monotonicity,
Essmonotonicity, NVP, Pareto principle, MooreRepullo condition, and so on) given the preference domain models.
These domains are small, restrictive or unrestrictive, profiles of the preference orderings.
The system has the prepared modelbases and the mechanisms which have been argued in the literature.
(More..)
 (working paper)
Implementing Nash Implementation Theory on Prolog: A Logic Programming Approach
(postscript 221KB)>
 (v)
A revision 2005/10/2811/16. (Prolog, impl13b.pl)
An extended version that incorporates Suh(1996)'s strong Nash implementation
and the code totally refined. (I abolish two previous versions impl13.pl and impl13a.pl
and replaced them with imple13b.pl)
 (an experimental result by test_impl/0)
( impl_suh.txt)
 (another data of the gMR2 and Condition mu(iv)
related rules revised) domain model mr.
( messages_1118.pl 862KB)
revision
10 Jan; 18 Mar; 7 May; 11 Jul; 5,19,27 Aug; 22 Nov (2007),
12 Mar; 211 May; 89 Jul; 8 Aug; 15 Sep (2008); 7 Feb; 23 Mar (2010); 5 Jan (2011).
&Copyright 20062011 Kenryo INDO
email: