Reseña: Developing an auction theory toolbox

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Developing an auction theory toolbox.

Sus autores son Christoph Lange, Colin Rowat, Wolfgang Windsteiger y Manfred Kerber.

Su resumen es

Auctions allocate trillions of dollars in goods and services every year. Auction design can have significant consequences, but its practice outstrips theory. We seek to advance auction theory with help from mechanised reasoning. To that end we are developing a toolbox of formalised representations of key facts of auction theory, which will allow auction designers to have relevant properties of their auctions machine-checked. As a first step, we are investigating the suitability of different mechanised reasoning systems (Isabelle, Theorema, and TPTP) for reproducing a key result of auction theory: Vickrey’s celebrated 1961 theorem on the properties of second price auctions – the foundational result in modern auction theory. Based on our formalisation experience, we give tentative recommendations on what system to use for what purpose in auction theory, and outline further steps towards a complete auction theory toolbox.

El trabajo se presentó en la AISB Convention 2013.

Los códigos de las correspondientes teorías se encuentran Auction Theory Toolbox (ATT). Contiene los códigos de las formalizaciones en CASL, Isabelle, Mizar y Theorema.