### Abstract

A VCG auction (named after their inventors Vickrey, Clarke, and Groves) is a generalization of the single-good, second price Vickrey auction to the case of a combinatorial auction (multiple goods, from which any participant can bid on each possible combination). We formalize in this entry VCG auctions, including tie-breaking and prove that the functions for the allocation and the price determination are well-defined. Furthermore we show that the allocation function allocates goods only to participants, only goods in the auction are allocated, and no good is allocated twice. We also show that the price function is non-negative. These properties also hold for the automatically extracted Scala code.

### License

BSD License

### Topics

- Mathematics/Games and economics

### Session Vickrey_Clarke_Groves

- SetUtils
- Partitions
- Argmax
- RelationOperators
- RelationProperties
- MiscTools
- StrictCombinatorialAuction
- Universes
- UniformTieBreaking
- CombinatorialAuction
- CombinatorialAuctionCodeExtraction
- FirstPrice
- CombinatorialAuctionExamples

## Cite

×

Vickrey_Clarke_Groves-AFP

    @article{Vickrey_Clarke_Groves-AFP,
      author  = {Marco B. Caminati and Manfred Kerber and Christoph Lange and Colin Rowat},
      title   = {VCG - Combinatorial Vickrey-Clarke-Groves Auctions},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Vickrey_Clarke_Groves.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- May 9, 2015 : Isabelle2014
- Apr 30, 2015 : Isabelle2014