TY - GEN
T1 - The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema
AU - Maletzky, Alexander
AU - Windsteiger, Wolfgang
PY - 2017/7
Y1 - 2017/7
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/85025144224
U2 - 10.1007/978-3-319-62075-6_3
DO - 10.1007/978-3-319-62075-6_3
M3 - Conference proceedings
SN - 9783319620749
VL - 10383
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 25
EP - 39
BT - Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21
A2 - Hasan, Osman
A2 - Rabe, Florian
A2 - Geuvers, Herman
A2 - Teschke, Olaf
A2 - England, Matthew
PB - Springer
ER -