Simulating Nash implementation under social choice environment by Prolog

updated: 12 Feb 2006

This is a page of STMD (Simulating Theoretical Models of Decision Making by Prolog and Spreadsheet), my Lab. on decision making and so on. I have been developing a series of prolog programs which models and simulates the Nash implementation theory since 2001. The development during 2001- 2002 and the modifications have done in 2003, 2005, using SWI-prolog 5.1.0(5.0.9).
The strategy is a generate-and-test method that for given a (rather small) preference domain models, it makes the possible SCC(social choice correspondings) and verifies several prerequisite conditions for Nash implementability, such as Maskin monotonicity, Ess-monotonicity, NVP, Pareto principle and so on.
If domains are suffiently small, you can compute the SCCs with desirable properties, for restrictive or unrestrictive preference orderings. The system also has the prepared modelbases and the simulation scripts of the mechanisms which have been argued in the literature.

Papers and Prolog source code

working paper

Implementing Nash Implementation Theory on Prolog: A Logic Programming Approach (postscript 221KB)> Reported in the 6th experimental economic conference 2003 at Chiba Keiai University.

source code

A revision 2005/10/28-11/16. (Prolog,
An extended version that incorporates Suh(1996)'s strong Nash implementation and the code totally refined. (I abolish two previous versions and and replaced them with

experimental data

Other versions

Main Components of the System

The prolog program simulates `scc's defined over small (restrictive or unrestrictive) preference domain. You may generate sccs with or without specified some prerequisite conditions over possible sccs such as monotonicity. And I have prepared several mechanisms in the literature and the experimetal scripts for simulating Nash implmentability as follows:

domain modeling (agent system)

social choice correspondence (Scc)

mechanisms (the message spaces and the game forms)



Some examples in the literature are not fully implemented in this simulation program. For example, as for Moore and Repullo(1991)'s 2-person example, (s2,c) is out of SCC but the program find a Nash equilibrium by using a simulated Moore-Repullo mechanism gMR2. See figure below.
This problem had been unresolved until Nov 2005. I the version impl13b, I had revised my code for gMR2's game forms using select_common_maximal_element_in_scc/3 instead of mre/5 which was erroneous code to select an alternative conforming condition mu2 (iv). (17 Nov 2005.)

the provision

The code for condition mu(iv) was correct, however, mre/5 had to be corrected. I fixed this bug and in the second rule of gMR2 where new rule select_common_maximal_element_in_scc/3 (instead of mre/5) which does not produce c but z if the true state is s2 with the reported profile of (s3,s4) above. I'm sorry for so long time to detect it.
?- prefer_profile([1,2],s3,M),
Ms=[1:(M,c,a,0,0),2:(M1,c,a,0,0)],   % for new version 
%Ms=[(M,c,a,0,0),(M1,c,a,0,0)],   % for earlier versions

For state s2, outcome c  [out, mr], rule 2  
and message profile: 
 1: ([[a, c, d, b, z], [b, d, c, a, z]], c, a, 0, 0)
 2: ([[a, d, c, b, z], [b, c, d, a, z]], c, a, 0, 0)

 agents=[1],Pzs=[1, 2, 3],Czs=[b, c, z],Lcc=[b, c, z] 
agents=[2],Pzs=[1, 2, 4],Czs=[a, c, z],Lcc=[a, c, z]
best response groups: [[1], [2]] This action profile is a Nash equilibrium. M = [[a, c, d, b, z], [b, d, c, a, z]] M1 = [[a, d, c, b, z], [b, c, d, a, z]] Ms = [1: ([[a, c, d, b, z], [b, d, c, a|...]], c, a, 0, 0), 2: ([[a, d, c, b|...], [b, c, d|...]], c, a, 0, 0)] Yes ?-
Figure 1. An untruthful equilibrium in the model 'mr' with the mechanism gMR2.


When using Danilov's mechanism gD applied for a Pareto correspondence under 2-person 2-outcomes unristricted domain ('ud22'), it is implemeted.

the provision

not yet.


Partially. This code has tested by SWI-Prolog 1.9.0 and 5.0.9 developed by J. Wielemaker, Amsterdam University and maintained by No legitimate test of compatibility for other Edinburgh- or ISO- PROLOG has been done. But the current version impl13 has almost ISO-compatible (probabiliy) except for a few SWI-proper predicate.

complexity and trouble in the run

Even though small domain, it may impossible to enumerate all sccs or to verify implementability using some mechanism directly computing Nash equilibria.
The system has some provisions for these problems, although not sufficient. ( For example, the 0-mode for test_impl, or test_nash which presets the integer parts of the messages in mechanism instead of the full(_) mode.) The `truthful(0)' mode provides simple simulation instead of the full-mode simulation.
In order to terminate the SWI-Prolog window, use the standard procedure for Windows OS. (Windows XP is recommended.) By Ctrl+C, you can stop during the execution. But if it needs to kill the process, using task manager and terminate plwin.exe.

Address of author

Department of Management, Faculty of Economics, Kanto Gakuen University.
200 Fujiagu, Ota si, Gunma ken, 373-8515 Japan. e-mail: