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: 4 Jun 2019

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.

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 sign-based 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 Arrow-type result for weak ordering (fixed in cswf07). Bug fix for dictatorship and rewrite for several Pareto conditions (fixed in cswf08).
automated proofs for the Gibbard-Satterthwaite's SCF (spsc06, revised 26 Dec 2006; 3 Sep 2009) Pareto condition is corrected.
common admissible domain and decomposability (Kalai-Muller theorem) ( dcdi06, revised 6 Jan 2007)
common (or individual) admissible domains: single-peakedness, 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), Blair-Muller(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. 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.

Paper

papers and slides

Parallel Possibility Results of Preference Aggregation and Strategy-proofness by using Prolog. DOI: 10.5220/0004913302430248 In Proceedings of the 6th International Conference on Agents and Artificial Intelligence (ICAART-2014), pages 243-248. poster, source code, and so on

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

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 strategic-proof 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 strategic-proof social choice function (v) (sproof.pl, Prolog, 13 Jan 2006) 2-person and 3-alternative case of the Gibbard-Satterthwaite theorem. Generating SP-obeying SCFs by means of recursive construction with MM (Maskin-monotonicity) 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) 2-person and 3-alternative 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 re-modeling 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 displaying-swf command in swd_d.pl ((source code)) and figures which show the patterns of IIA-equivalent profiles (iia_profiles.txt).

Simulation of Nash implementation under abstract social choice environment (2001-2002,2005)
The prolog program which generates the possible SCC(social choice correspondings) and verifies several prerequisite conditions for Nash implementability (such as Maskin monotonicity, Ess-monotonicity, NVP, Pareto principle, Moore-Repullo 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/28-11/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; 2-11 May; 8-9 Jul; 8 Aug; 15 Sep (2008); 7 Feb; 23 Mar (2010); 5 Jan (2011).