Computer-Aided Theorem Discovery - A New Adventure and its Application to Economic Theory

The Hong Kong University of Science and Technology
Department of Computer Science and Engineering


PhD Thesis Defence


Title: "Computer-Aided Theorem Discovery -
A New Adventure and its Application to Economic Theory"

By

Mr. Pingzhong Tang


Abstract

Theorem discovery, with the help of computer, presents at least two steps 
of challenges. The first concerns how to come up with reasonable 
conjectures automatically. This raises further challenges, such as how to 
represent these conjectures within the computers, what is the yardstick 
for reasonableness, etc. The second concerns how to prove or negate the 
conjectures automatically. However theorem proving, even for the best of 
human beings, is still an intelligence-demanding endeavor and sometimes 
even a nightmare.

Our starting point however, is a basic form of proof, namely proof by 
induction. The heuristic behind is extremely straightforward: We first 
formulate the problem domain in a proper language, say logic or other 
formal languages. We then enumerate the sentences (within certain length 
limit) in the underlying language that describe propositions in the 
domain. After that, we use a computer program to verify through these 
sentences to find those true in base cases, that is, where the problem 
size is small. The remaining sentences serves as conjectures, which can be 
extended, one way or other, to inductive cases.

It turns out that this methodology has been quite effective since we 
adopted it in economic theory. In particular, some of our programs on game 
theory have returned theorems that shed lights on the understanding of 
basic game forms such as zero-sum game, potential game and super-modular 
game. Some of them have helped us prove some Nobel Prize winning theorems 
such as Arrow's impossibility theorem and Sen's theorem on voting 
functions and discover new theorems that better characterize key concepts 
in social choice theory. Others also have helped us prove Nobel Prize 
winning theorems such as Maskin's theorem on Nash implementation as well 
as Gibbard-Satterthwaite theorem on dominant strategy implementation. 
These proofs themselves also provide insights on discovering similar 
theorems.

This thesis reports all attempts that we have conducted in the past few 
years, in support of the general methodology of theorem discovery.


Date:			Monday, 17 May 2010

Time:			2:00pm – 4:00pm

Venue:			Room 5508
 			Lifts 25/26

Chairman:		Prof. Hoi Sing Kwok (ECE)

Committee Members:	Prof. Fangzhen Lin (Supervisor)
 			Prof. Ke Yi
                       	Prof. Nevin Zhang
                         Prof. Shiu Yuen Cheng (MATH)
                         Prof. Johannes van Benthem (Univ. of Amsterdam)


**** ALL are Welcome ****