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

PhD Thesis Proposal 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 us 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 on social choice theory have
proved Nobel Prize winning theorems such as Arrow's impossibility
theorem and Sen's theorem on democratic voting schemes and discover
new theorems that better characterize concepts that play central
roles in the theory. Others on mechanism design theory have also
proved 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 manuscript simply reports all attempts that we have conducted
in the past a few years, in search of an elegant means to describe
this methodology.


Date:     		Monday, 31 August 2009

Time:                   3:00pm - 5:00pm

Venue:                  Room 3315
 			lifts 17-18

Committee Members:      Prof. Fangzhen Lin (Supervisor)
 			Prof. Nevin Zhang (Chairperson)
 			Dr. Ke Yi
 			Prof. Shiu-Yuen Cheng (MATH)


**** ALL are Welcome ****