Discovering Theorems in Game Theory: Two-Person Games with Unique Pure Nash Equilibrium Payoffs

We consider all possible games that have unique PNE payoffs. Our starting point is the classes of games that can be expressed by a conjunction class of two-person strictly competitive games. We first formulate of two binary clauses, and our program rediscovered the notions of games, strictly competitive games and Kats and Thisse's class of weakly unilaterally PNEs in first-order logic. Under our formulation, a class of competitive two-person games, and came games corresponds to a first-order sentence. In particular, the up with several other classes of games that have sentence that corresponds to the class of strictly competitive unique pure Nash equilibrium payoffs. It also came games is a conjunction of two binary clauses with all variables up with new classes of strict games that have unique universally quantified. So we implemented a program pure Nash equilibria, where a game is strict if for that examines all these universally quantified conjunctions of both player different profiles have different payoffs.