English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

When faced with the question of how to represent properties in a formal proofsystem any user has to make design decisions. We have proved three of thetheorems from Maskin's 2004 survey article on Auction Theory using theIsabelle/HOL system, and we have produced verified code for combinatorialVickrey auctions. A fundamental question in this was how to represent somebasic concepts: since set theory is available inside Isabelle/HOL, whenintroducing new definitions there is often the issue of balancing the amount ofset-theoretical objects and of objects expressed using entities which are moretypical of higher order logic such as functions or lists. Likewise, a user hasoften to answer the question whether to use a constructive or anon-constructive definition. Such decisions have consequences for the proofdevelopment and the usability of the formalization. For instance, sets areusually 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 theseapproaches and their relationships. In addition, we present the correspondingIsabelle library of definitions and theorems, most prominently those dealingwith relations and quotients.

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