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

DOI10.1007/978-3-319-62075-6_3zbMATH Open1367.68252OpenAlexW2729182356MaRDI QIDQ2364696FDOQ2364696

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

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

Mathematics Subject Classification ID

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

Cites Work

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Title not available (Why is that?)
• Mizar: state-of-the-art and beyond
• Title not available (Why is that?)
• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

Cited In (3)

• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
• Title not available (Why is that?)
• Set theory or higher order logic to represent auction concepts in Isabelle?

Uses Software

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

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)