The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
Conference for Intelligent Computer Mathematics (CICM)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
In earlier work presented at CICM, four theorem provers (Isabelle, Mizar, Hets/CASL/TPTP, and Theorema) were compared based on a case study in theoretical economics,
the formalization of the landmark Theorem of Vickrey in auction theory. At the time of this comparison the Theorema system
was in a state of transition: The original Theorema system (Theorema 1) had been shut down by the Theorema group and the successor system
Theorema 2.0 was just about to be launched. Theorema 2.0 participated in the competition, but only parts of the system were ready
for use. In particular, the new reasoning engines had not been set up, so that some of the results in the system comparison had
to be extrapolated from experience we had with Theorema 1. In this paper, we now want to compare a complete formalization of Vickrey's Theorem in
Theorema 2.0 with the original formalization in Isabelle. On the one hand, we compare the mathematical setup of the two theories and, on the other hand, we also
give an overview on statistical indicators, such as number of auxiliary lemmas
and the total number of proof steps needed for all proofs in the theory.
Last but not least, we present a shorter version of proof of the main theorem
in Isabelle.