{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T08:28:25Z","timestamp":1758702505265},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642393198"},{"type":"electronic","value":"9783642393204"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39320-4_13","type":"book-chapter","created":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T11:22:52Z","timestamp":1372677772000},"page":"200-215","source":"Crossref","is-referenced-by-count":11,"title":["A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Lange","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco B.","family":"Caminati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manfred","family":"Kerber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Till","family":"Mossakowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"Rowat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Makarius","family":"Wenzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Windsteiger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof General: A Generic Tool for Proof Development. In: Graf, S. (ed.) TACAS 2000. LNCS, vol.\u00a01785, pp. 38\u201343. Springer, Heidelberg (2000)"},{"key":"13_CR2","unstructured":"Auctions: The Past, Present and Future, \n                    \n                      http:\/\/realestateauctionglobalnetwork.blogspot.co.uk\/2011\/11\/auctions-past-present-and-future.html"},{"key":"13_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11812289_21","volume-title":"Mathematical Knowledge Management","author":"G. Bancerek","year":"2006","unstructured":"Bancerek, G.: Information Retrieval and Rendering with MML Query. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 266\u2013279. Springer, Heidelberg (2006)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Caminati, M.B., Rosolini, G.: Custom automations in Mizar. Automated Reasoning\u00a050(2) (2013)","DOI":"10.1007\/s10817-012-9266-1"},{"key":"13_CR5","unstructured":"CASL, \n                    \n                      http:\/\/informatik.uni-bremen.de\/cofi\/wiki\/index.php\/CASL"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Conitzer, V., Sandholm, T.: Self-interested automated mechanism design and implications for optimal combinatorial auctions. In: Conference on Electronic Commerce. ACM (2004)","DOI":"10.1145\/988772.988793"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Cramton, P., Shoham, Y., Steinberg, R. (eds.): Combinatorial auctions. MIT Press (2006)","DOI":"10.7551\/mitpress\/9780262033428.001.0001"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Farmer, W.M.: The seven virtues of simple type theory. Applied Logic\u00a06(3) (2008)","DOI":"10.1016\/j.jal.2007.11.001"},{"key":"13_CR9","unstructured":"Geanakoplos, J.D.: Three brief proofs of Arrow\u2019s impossibility theorem. Discussion Paper 1123RRR. Cowles Foundation (2001)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Geist, C., Endriss, U.: Automated search for impossibility theorems in social choice theory: ranking sets of objects. Artificial Intelligence Research\u00a040 (2011)","DOI":"10.1613\/jair.3126"},{"key":"13_CR11","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a Nutshell. Formalized Reasoning\u00a03(2) (2010)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0055133","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Griffioen","year":"1998","unstructured":"Griffioen, D., Huisman, M.: A comparison of PVS and isabelle\/HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 123\u2013142. Springer, Heidelberg (1998)"},{"key":"13_CR13","unstructured":"Initiative for Computational Economics, \n                    \n                      http:\/\/ice.uchicago.edu"},{"key":"13_CR14","unstructured":"Isabelle, \n                    \n                      http:\/\/isabelle.in.tum.de"},{"key":"13_CR15","unstructured":"Kerber, M., Lange, C., Rowat, C.: An economist\u2019s guide to mechanized reasoning (2012), \n                    \n                      http:\/\/cs.bham.ac.uk\/research\/projects\/formare\/"},{"key":"13_CR16","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-22673-1_5","volume-title":"Intelligent Computer Mathematics","author":"M. Kerber","year":"2011","unstructured":"Kerber, M., Rowat, C., Windsteiger, W.: Using Theorema in the Formalization of Theoretical Economics. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS (LNAI), vol.\u00a06824, pp. 58\u201373. Springer, Heidelberg (2011)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Kirkegaard, R.: A Mechanism Design Approach to Ranking Asymmetric Auctions. Econometrica\u00a080(5) (2012)","DOI":"10.3982\/ECTA9859"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Klemperer, P.: Auctions: theory and practice. Princeton Univ. Press (2004)","DOI":"10.1515\/9780691186290"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Klemperer, P.: The product-mix auction: a new auction design for differentiated goods. European Economic Association Journal\u00a08(2-3) (2010)","DOI":"10.1111\/j.1542-4774.2010.tb00523.x"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Korni\u0142owicz, A.: On Rewriting Rules in Mizar. Automated Reasoning\u00a050(2) (2013)","DOI":"10.1007\/s10817-012-9261-6"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Lamport, L., Paulson, L.C.: Should your specification language be typed? ACM TOPLAS\u00a021(3) (1999)","DOI":"10.1145\/319301.319317"},{"key":"13_CR22","series-title":"LNAI","first-page":"330","volume-title":"CICM 2013","author":"C. Lange","year":"2013","unstructured":"Lange, C., Rowat, C., Kerber, M.: The ForMaRE Project \u2013 Formal Mathematical Reasoning in Economics. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 330\u2013334. Springer, Heidelberg (2013)"},{"key":"13_CR23","unstructured":"Lange, C., et al.: Auction Theory Toolbox (2013), \n                    \n                      http:\/\/cs.bham.ac.uk\/research\/projects\/formare\/code\/auction-theory\/"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Maskin, E.: The unity of auction theory: Milgrom\u2019s master class. Economic Literature\u00a042(4) (2004)","DOI":"10.1257\/0022051043004586"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Milgrom, P.: Putting auction theory to work. Cambridge Univ. Press (2004)","DOI":"10.1017\/CBO9780511813825"},{"key":"13_CR26","unstructured":"Mizar manuals (2011), \n                    \n                      http:\/\/mizar.org\/project\/bibliography.html"},{"key":"13_CR27","unstructured":"Mossakowski, T.: Hets: the Heterogeneous Tool Set, \n                    \n                      http:\/\/dfki.de\/cps\/hets"},{"key":"13_CR28","unstructured":"Mossakowski, T., Maeder, C., Codescu, M.: Hets User Guide. Tech. rep. Version 0.98. DFKI Bremen (2013), \n                    \n                      http:\/\/informatik.uni-bremen.de\/agbkb\/forschung\/formal_methods\/CoFI\/hets\/UserGuide.pdf"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"CASL Reference Manual","year":"2004","unstructured":"Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol.\u00a02960. Springer, Heidelberg (2004)"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Social choice theory in HOL: Arrow and Gibbard-Satterthwaite. Automated Reasoning 43(3) (2009)","DOI":"10.1007\/s10817-009-9147-4"},{"key":"13_CR31","unstructured":"Rudnicki, P., Urban, J., et al.: Escape to ATP for Mizar. In: Workshop Proof eXchange for Theorem Proving (2011)"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Automated Reasoning 43(4) (2009)","DOI":"10.1007\/s10817-009-9143-8"},{"key":"13_CR33","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-642-28717-6_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Sutcliffe","year":"2012","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP Typed First-order Form with Arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18. LNCS (LNAI), vol.\u00a07180, pp. 406\u2013419. Springer, Heidelberg (2012)"},{"key":"13_CR34","unstructured":"System on TPTP, \n                    \n                      http:\/\/cs.miami.edu\/~tptp\/cgi-bin\/SystemOnTPTP"},{"key":"13_CR35","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-540-93920-7_13","volume-title":"Declarative Agent Languages and Technologies VI","author":"E.M. Tadjouddine","year":"2009","unstructured":"Tadjouddine, E.M., Guerin, F., Vasconcelos, W.: Abstracting and Verifying Strategy-Proofness for Auction Mechanisms. In: Baldoni, M., Son, T.C., van Riemsdijk, M.B., Winikoff, M. (eds.) DALT 2008. LNCS (LNAI), vol.\u00a05397, pp. 197\u2013214. Springer, Heidelberg (2009)"},{"key":"13_CR36","doi-asserted-by":"crossref","unstructured":"Tang, P., Lin, F.: Computer-aided proofs of Arrow\u2019s and other impossibility theorems. Artificial Intelligence\u00a0173(11) (2009)","DOI":"10.1016\/j.artint.2009.02.005"},{"key":"13_CR37","doi-asserted-by":"crossref","unstructured":"Tang, P., Lin, F.: Discovering theorems in game theory: two-person games with unique pure Nash equilibrium payoffs. Artificial Intelligence 175(14-15) (2011)","DOI":"10.1016\/j.artint.2011.07.001"},{"key":"13_CR38","doi-asserted-by":"crossref","unstructured":"Urban, J.: MizarMode\u2014an integrated proof assistance tool for the Mizar way of formalizing mathematics. Applied Logic\u00a04(4) (2006)","DOI":"10.1016\/j.jal.2005.10.004"},{"key":"13_CR39","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-642-31374-5_38","volume-title":"Intelligent Computer Mathematics","author":"M. Wenzel","year":"2012","unstructured":"Wenzel, M.: Isabelle\/jEdit \u2013 a Prover IDE within the PIDE framework. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol.\u00a07362, pp. 468\u2013471. Springer, Heidelberg (2012)"},{"key":"13_CR40","unstructured":"Wiedijk, F.: De Bruijn factor, \n                    \n                      http:\/\/cs.ru.nl\/~freek\/factor\/"},{"key":"13_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-24849-1_24","volume-title":"Types for Proofs and Programs","author":"F. Wiedijk","year":"2004","unstructured":"Wiedijk, F.: Formal proof sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 378\u2013393. Springer, Heidelberg (2004)"},{"key":"13_CR42","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Formalizing Arrow\u2019s theorem. S\u0101dhan\u0101 34(1) (2009)","DOI":"10.1007\/s12046-009-0005-1"},{"key":"13_CR43","unstructured":"Wiedijk, F.: The QED Manifesto Revisited. Studies in Logic, Grammar and Rhetoric\u00a010(23) (2007)"},{"key":"13_CR44","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"},{"key":"13_CR45","unstructured":"Wikipedia (ed.): Vickrey auction (2012), \n                    \n                      http:\/\/en.wikipedia.org\/w\/index.php?title=Vickrey_auction&oldid=523230741"},{"key":"13_CR46","doi-asserted-by":"crossref","unstructured":"Windsteiger, W.: Theorema 2.0: A Graphical User Interface for a Mathematical Assistant System. In: UITP Workshop at CICM (2012)","DOI":"10.4204\/EPTCS.118.5"},{"key":"13_CR47","doi-asserted-by":"crossref","unstructured":"Woodcock, J., et al.: Formal method: practice and experience. ACM Computing Surveys\u00a041(4) (2009)","DOI":"10.1145\/1592434.1592436"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39320-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T06:12:54Z","timestamp":1557900774000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39320-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642393198","9783642393204"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39320-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}