This paper pursues the perspective of Lin [11,12] that many interesting theorems can be automatically discovered by
first specifying a class of conjectures in a logical language and then testing them systematically in some small domains. This
approach presents at least two challenges. The first concerns how to come up with a set of reasonable conjectures. This
raises further issues, such as how to represent these conjectures, what is the yardstick for reasonableness, etc. The second
concerns how to prove or refute the conjectures automatically.
In general, using computers to discover theorems is a difficult endeavor. Nonetheless there have been various attempts.
In one pioneer work, Petkovsek et al. [15] showed that to prove the following theorem,
“The angle bisectors of every triangle intersect at one point”,
it suffices to verify it in 64 non-isomorphic triangles, which can be automated by computers. In the same spirit, the authors
went on to demonstrate that certain forms of theorems concerning the close form of the sum of combinatorial sequences
can be completely discovered by computers programs.
Langley [5] had briefly summarized the attempts of computer-aided discovery until 1998, ranging from mathematics to
physics, chemistry as well as biology. Among those attempts, Lenat’s AM system [6] and Fajtlowicz’s Graffiti [2] are also
remarkable progresses on theorem discovery. The AM system aims at finding new concepts and theorems based on existing
concepts as well as a large amount of heuristic rules, which require extensive domain knowledge of the designers. Despite the complexity of design, the system managed to rediscover hundreds of common concepts as well as simple theorems.
The Graffiti system, on the other hand, is more intuitive in design. First of all, the system itself does not attempt to prove
anything. Alternatively, it aims at generating interesting conjectures in graph theory by guessing and testing some invariants,
most of which are of forms a b, a = b, and ai bi , concerning two numerical features in a graph. It is worth some
attention that Graffiti maintains the quality of the set of conjectures by filtering those implied by existing ones. In other
words, the current set of conjectures are the strongest ones generated so far. This is similar to our approach in game theory,
which will be introduced in detail later.
Our work here continues the line of work in [11,9]. In both papers, the problem domain is formulated in a symbolic
language. Conjectures about the domains are then represented by sentences in the underlying language. A computer program
is then used to test through these conjectures to find those that are true in domains up to certain small size. These
conjectures are either guaranteed to be true in the general case or checked manually. A parallel work applies the same
idea on social-choice theory [10,17], where we prove three of the most important impossibility theorems in a unified
computer-aided framework. We also similarly discover several theorems that generalize Arrow’s conditions as well as a
new theorem that better interprets Arrow’s IIA condition. Interestingly, this approach has recently been proved effective
in finding impossibility theorems in another field of social choice [3]. Similar idea can be found in automated mechanism
design [7,8], where they use several parameters as domain language to describe a class of auctions and then search through
the language to find the revenue-optimal auctions.
In this paper, we will show how the same methodology can be used to discover some interesting theorems about pure
Nash equilibria. Traditional equilibrium analysis has been mostly focused on mixed strategy equilibria. Part of the reasons
for this bias is that such an equilibrium always exists and algorithms such as the one by Lemke–Howson are guaranteed to
find one. Moreover, best response functions in games with mixed strategies are continuous and differentiable, allowing for
standard calculus techniques to be applied.
However, pure Nash equilibria (PNEs) are also of interest, and there is already much work about them. Examples here include
the existence of PNEs in ordinal potential games [13], quasi-supermodular games [20] as well as games with dominant
strategies, and uniqueness of PNE payoffs1 in two-person strictly competitive games [14].
As part of our project on using computers to discover theorems in game theory, this paper considers the possibility of
using computers to discover new classes of two-person games that have unique PNE payoffs. Here is an overview of our
project.• Step 1. We first formulate the notions of games, strictly competitive games and PNEs in first-order logic. Under our
formulation, a class of games corresponds to a first-order sentence.
• Step 2. We then consider sentences that have similar syntactic form as that of strictly competitive games.
• Step 3. We prove that a sentence of this form is a sufficient condition for a game to have a unique PNE payoff iff it is
so for all 2×2 games.
• Step 4. We then generate all sentences of the form in step 2, and check if any of them is a sufficient condition for a
2×2 game to have unique PNE payoff.
• Step 5. Finally, among these sufficient conditions, we collect weakest ones.
We did not expect much as these conditions are rather simple, but to our surprise, our program returned a condition
that is more general than the strict competitiveness condition. As it turned out, it exactly corresponds to Kats and Thisse’s
[4] class of weakly unilaterally competitive two-person games. Our program also returned some other conditions. Two of
them capture a class of “unfair” games where one player has advantage over the other. The remaining ones capture games
where everyone gets what he wants – each receives his maximum payoff in every equilibrium state, thus there is no real
competition among the players. Thus one conclusion that we can draw from this experiment is that among all classes of
games that can be expressed by a conjunction of two binary clauses, the class of weakly unilaterally competitive games is
the most general class of “competitive” and “fair” games that have unique PNE payoffs. Of course, this does not mean that
the other conditions are not worth investigating. For instance, sometimes one may be forced to play an unfair game.
For the same set of conditions, we also consider strict two-person games where different profiles have different payoffs
for each player. Among the results returned by our program, two of them are exactly the two conjuncts in Kats and Thisse’s
weakly unilaterally competitive condition, but the others all turn out to be special cases of games with dominant strategies.
Motivated by these results, we consider certain equivalent classes of games, and show that a strict game has a unique PNE
iff it is best-response equivalent [16] to a strictly competitive game. This turns out to be a new and interesting result, and
has recently been published in Games and Economic Behavior [18].
The rest of the paper is organized as follows. We first review some basic concepts in two-person games in strategic form,
and then reformulate them in first-order logic. We then show that for a class of conditions, whether any of them entails
the uniqueness of PNE payoff needs only to be checked on games up to certain size. We then describe a computer program
based on this result, and report our experimental results.
We have provided a logical framework for computer-aided theorem discovery in two-person game theory, and applied
it successfully to the task of discovering classes of two-person games with unique PNE payoffs. Our program returned a
condition that is more general than the strict competitiveness condition, namely, the weakly unilaterally competitiveness.
Two conditions, which we coin “I-compete-you-cooperate”, capture a class of “unfair” games where one player has advantage
over the other. The remaining ones capture games where everyone gets what he wants – each receives his maximum payoff in every equilibrium state, thus there is no real competition among the players. Thus one conclusion that we can draw from
this experiment is that among all classes of games that can be expressed by a conjunction of two binary clauses, the class
of weakly unilaterally competitive games is the most general class of “competitive” and “fair” games that have unique PNE
payoffs.
For the same set of conditions, we also consider strict two-person games where different profiles have different payoffs
for each player. Among the results returned by our program, two of them are exactly the two conjuncts in Kats and Thisse’s
weakly unilaterally competitive condition, but the others all turn out to be special cases of games with dominant strategies;
others correspond to games with dominant strategies. Motivated by these results, we consider certain equivalent classes of
games, and show that a strict game has a unique PNE iff it is best-response equivalent to a strictly competitive game.
There are many directions for future work. An obvious one is to see how interesting theorems can be discovered using
Theorem 1 on classes of games that do not have any PNE and games whose PNEs are Pareto optimal. More importantly, we
would like to see how this methodology can be applied on classes of game that has at least one PNE. In fact, we recently
have found that two such classes, potential games and supermodular games are best response equivalent [18]. Our program
also shows there are other classes of games that do not belong to either class but still have at least one PNE. This suggests a
new research direction: a characterization of these games. An even more interesting direction is to come up with a language
that can effectively represent mix strategy equilibria and then conduct our theorem discovery method on this setting.
