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

DOI10.1007/978-3-319-62075-6_3MaRDI QIDQ2364696zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
• Set theory or higher order logic to represent auction concepts in Isabelle?
• Using Theorema in the Formalization of Theoretical Economics
• An introduction to mechanized reasoning
• Formalizing Arrow's theorem

Cites work

• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• scientific article; zbMATH DE number 2172806 (Why is no real title available?)
• Mizar: state-of-the-art and beyond
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Cited in

(3)

• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
• scientific article; zbMATH DE number 1884390 (Why is no real title available?)
• Set theory or higher order logic to represent auction concepts in Isabelle?

Describes a project that uses

Uses Software

• Vickrey_Clarke_Groves
• Isabelle
• Theorema
• Isar
• Hets
• Archive of Formal Proofs
• Isabelle/Isar
• CASL
• TPTP
• Mizar

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2364696)