×

zbMATH — the first resource for mathematics

Set theory or higher order logic to represent auction concepts in Isabelle? (English) Zbl 1304.68152
Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 236-251 (2014).
Summary: 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 E. Maskin’s survey article on auction theory [“The unity of auction theory: Milgrom’s master class”, Journal of Economic Literature 42, No. 4, 1102–1115 (2004; doi:10.1257/0022051043004586)] 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 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. 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.
For the entire collection see [Zbl 1293.68035].
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T30 Knowledge representation
91B26 Auctions, bargaining, bidding and selling, and other market models
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bergman, C.: Universal Algebra: Fundamentals and Selected Topics. Chapman & Hall Pure and Applied Mathematics. Taylor & Francis (2011)
[2] Blanchette, J.C., Paulson, L.C.: Hammering Away. A User’s Guide to Sledgehammer for Isabelle/HOL (December 5, 2013), http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/sledgehammer.pdf
[3] Bowen, J., Gordon, M.: Z and HOL. In: Z User Workshop, Cambridge 1994, pp. 141–167. Springer (1994)
[4] Caminati, M.B., et al.: Proving soundness of combinatorial Vickrey auctions and generating verified executable code, arXiv:1308.1779 [cs.GT] (2013)
[5] Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010) · Zbl 1284.68131
[6] Klein, G., et al. (eds.): Archive of Formal Proofs (2014), http://afp.sf.net/ (visited on March 14, 2014)
[7] Lange, C., Caminati, M.B., Kerber, M., Mossakowski, T., Rowat, C., Wenzel, M., Windsteiger, W.: A qualitative comparison of the suitability of four theorem provers for basic auction theory. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 200–215. Springer, Heidelberg (2013) · Zbl 1390.68577
[8] Lange, C., Rowat, C., Kerber, M.: The ForMaRE Project – Formal Mathematical Reasoning in Economics. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 330–334. Springer, Heidelberg (2013), arXiv:1303.4194[cs.CE] · Zbl 1390.68578
[9] Leinster, T.: Rethinking set theory. arXiv preprint arXiv:1212.6543 (2012)
[10] Maskin, E.: The unity of auction theory: Milgrom’s master class. Journal of Economic Literature 42(4), 1102–1115 (2004), http://scholar.harvard.edu/files/maskin/files/unity_of_auction_theory.pdf
[11] Nipkow, T., Paulson, L.C.: Proof pearl: Defining functions over finite sets. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 385–396. Springer, Heidelberg (2005) · Zbl 1152.68529
[12] Paulson, L.C.: Defining functions on equivalence classes. ACM Transactions on Computational Logic (TOCL) 7(4), 658–675 (2006) · Zbl 1367.68254
[13] Paulson, L.C.: Set Theory for Verification: I. From Foundations to Functions. Journal of Automated Reasoning 11, 353–389 (1993) · Zbl 0802.68128
[14] Paulson, L.C., et al.: Isabelle/HOL. A Proof Assistant for Higher-Order Logic (2013) · Zbl 0994.68131
[15] Simpson, S.G.: Subsystems of second order arithmetic, vol. 1. Cambridge University Press (2009) · Zbl 1181.03001
[16] Valentine, S.H., et al.: AZ Patterns Catalogue II-definitions and laws, v0.1 (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.