Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. Set theory or higher order logic to represent auction concepts in Isabelle?
 Watt, S.M.: Intelligent computer mathematics. International conference, CICM 2014 : Coimbra, Portugal, July 711, 2014; Proceedings Cham: Springer International Publishing, 2014 (Lecture Notes in Computer Science 8543) ISBN: 9783319084336 ISBN: 9783319084343 S.236251 
 International Conference on Intelligent Computer Mathematics (CICM) <2014, Coimbra> 

 Englisch 
 Konferenzbeitrag 
 Fraunhofer IAIS () 
Abstract
When faced with the question of how to represent properties in a formal proof system any user has to make design decisions. We have proved three of the theorems from Maskin's 2004 survey article on Auction Theory using the Isabelle/HOL system, and we have verified software code that implements combinatorial Vickrey auctions. A fundamental question in this was how to represent some basic concepts: since set theory is available inside Isabelle/HOL, when introducing new definitions there is often the issue of balancing the amount of settheoretical objects and of objects expressed using entities which are more typical of higher order logic such as functions or lists. Likewise, a user has often to answer the question whether to use a constructive or a nonconstructive definition. Such decisions have consequences for the proof development and the usability of the formalization. For instance, sets are usually closer to the representation that economists would use and recognize, while the other objects are closer to the extraction of computational content. We have studied the advantages and disadvantages of these approaches, and their relationship, in the concrete application setting of auction theory. In addition, we present the corresponding Isabelle library of definitions and theorems, most prominently those dealing with relations and quotients.