The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema

DOI10.1007/978-3-319-62075-6_3zbMath1367.68252OpenAlexW2729182356MaRDI QIDQ2364696

Alexander Maletzky, Wolfgang Windsteiger

Publication date: 21 July 2017

Full work available at URL: https://doi.org/10.1007/978-3-319-62075-6_3

Mathematics Subject Classification ID

Auctions, bargaining, bidding and selling, and other market models (91B26)

Uses Software

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• TPTP
• Isar
• Mizar
• Hets
• Archive Formal Proofs
• Vickrey_Clarke_Groves

Cites Work

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
• Mizar: State-of-the-art and Beyond
• Unnamed Item
• Unnamed Item

This page was built for publication: The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema