{"id":4643,"date":"2014-12-09T06:44:28","date_gmt":"2014-12-09T05:44:28","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4643"},"modified":"2014-12-09T06:44:28","modified_gmt":"2014-12-09T05:44:28","slug":"resena-budget-imbalance-criteria-for-auctions-a-formalized-theorem","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-budget-imbalance-criteria-for-auctions-a-formalized-theorem\/","title":{"rendered":"Rese\u00f1a: Budget imbalance criteria for auctions: A formalized theorem"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre econom\u00eda titulado <a href=\"http:\/\/bit.ly\/1G4qKn2\">Budget imbalance criteria for auctions: A formalized theorem<\/a>.<\/p>\n<p>Sus autores son <a href=\"https:\/\/sites.google.com\/site\/marcocaminati\">Marco B. Caminati<\/a>, <a href=\"http:\/\/www.cs.bham.ac.uk\/~mmk\">Manfred Kerber<\/a> y <a href=\"http:\/\/www.socscistaff.bham.ac.uk\/rowat\">Colin Rowat<\/a> (de la Univ. de Birmingham).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle\/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas.\n<\/p><\/blockquote>\n<p>El trabajo se ha presentado en la <a href=\"http:\/\/bit.ly\/1GcFEG0\">6th Podlasie Conference on Mathematics 2014<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle se encuentra <a href=\"https:\/\/github.com\/formare\/auctions\/tree\/master\/isabelle\/Auction\/Maskin2-3\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre econom\u00eda titulado Budget imbalance criteria for auctions: A formalized theorem. Sus autores son Marco B. Caminati, Manfred Kerber y Colin Rowat (de la Univ. de Birmingham). Su resumen es We present an original theorem in auction theory: it specifies general conditions under which the&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[144,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4643"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4643"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4643\/revisions"}],"predecessor-version":[{"id":4644,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4643\/revisions\/4644"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4643"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4643"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4643"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}