Alexander Maletzky, Wolfgang Windsteiger,
"The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema"
, in H. Geuvers and M. England and O. Hasan and F. Rabe and O. Teschke: Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, Serie Lecture Notes in Computer Science (LNCS), Vol. 10383, Springer, Seite(n) 25-39, 7-2017, ISBN: 978-3-319-62075-6
Original Titel:
The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema
Sprache des Titels:
Englisch
Original Buchtitel:
Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21
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.
Forschungs-