Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?

Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)


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 produced verified code for 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 set-theoretical 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 non-constructive 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. In this paper we give examples of the advantages and disadvantages for these approaches and their relationships. In addition, we present the corresponding Isabelle library of definitions and theorems, most prominently those dealing with relations and quotients.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publicationInternational Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings
EditorsStephen M Watt, James H Davenport, Alan P Sexton, Petr Sojka, Josef Urban
Number of pages16
Volume8543 LNCS
ISBN (Electronic)9783319084343
ISBN (Print)9783319084336
Publication statusPublished - 7 Jul 2014
Event Conference on Intelligent Computer Mathematics -, Coimbra, United Kingdom
Duration: 7 Jul 201411 Jul 2014

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conference Conference on Intelligent Computer Mathematics
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?'. Together they form a unique fingerprint.

Cite this