{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:58:11Z","timestamp":1740099491766,"version":"3.37.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030290061"},{"type":"electronic","value":"9783030290078"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29007-8_14","type":"book-chapter","created":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T19:10:06Z","timestamp":1566414606000},"page":"240-256","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying Randomised Social Choice"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4263-6571","authenticated-orcid":false,"given":"Manuel","family":"Eberl","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,14]]},"reference":[{"issue":"2","key":"14_CR1","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/3125642","volume":"65","author":"F Brandl","year":"2018","unstructured":"Brandl, F., Brandt, F., Eberl, M., Geist, C.: Proving the incompatibility of efficiency and strategyproofness via SMT solving. J. ACM 65(2), 6:1\u20136:28 (2018)","journal-title":"J. ACM"},{"key":"14_CR2","unstructured":"Eberl, M.: Randomised social choice theory. Archive of Formal Proofs, formal proof development, May 2016"},{"key":"14_CR3","unstructured":"Eberl, M.: The incompatibility of SD-efficiency and SD-strategy-proofness. Archive of Formal Proofs, formal proof development, May 2016"},{"issue":"4","key":"14_CR4","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1086\/256963","volume":"58","author":"KJ Arrow","year":"1950","unstructured":"Arrow, K.J.: A difficulty in the concept of social welfare. J. Polit. Econ. 58(4), 328\u2013346 (1950)","journal-title":"J. Polit. Econ."},{"issue":"02","key":"14_CR5","doi-asserted-by":"publisher","first-page":"665","DOI":"10.2307\/1911681","volume":"45","author":"A Gibbard","year":"1977","unstructured":"Gibbard, A.: Manipulation of schemes that mix voting with chance. Econometrica 45(02), 665\u2013681 (1977)","journal-title":"Econometrica"},{"key":"14_CR6","unstructured":"Hales, T.C., et al.: A formal proof of the Kepler conjecture. \n                      arXiv:1501.0215\n                      \n                     (2015)"},{"issue":"12","key":"14_CR7","doi-asserted-by":"publisher","first-page":"1197","DOI":"10.1016\/S0764-4442(99)80439-X","volume":"328","author":"Warwick Tucker","year":"1999","unstructured":"Tucker, W.: The Lorenz attractor exists. Ph.D. thesis, Uppsala universitet (1999). Accessed 10 March 1999","journal-title":"Comptes Rendus de l'Acad\u00e9mie des Sciences - Series I - Mathematics"},{"issue":"3","key":"14_CR8","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/BF03025276","volume":"22","author":"M Viana","year":"2000","unstructured":"Viana, M.: What\u2019s new on Lorenz strange attractors? Math. Intell. 22(3), 6\u201319 (2000)","journal-title":"Math. Intell."},{"issue":"2","key":"14_CR9","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reasoning 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46669-8_4","volume-title":"Programming Languages and Systems","author":"M Eberl","year":"2015","unstructured":"Eberl, M., H\u00f6lzl, J., Nipkow, T.: A verified compiler for probability density functions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 80\u2013104. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46669-8_4"},{"key":"14_CR11","unstructured":"B\u00f6hme, S.: Proof reconstruction for Z3 in Isabelle\/HOL. In: 7th International Workshop on Satisfiability Modulo Theories (SMT 2009) (2009)"},{"key":"14_CR12","unstructured":"Espinoza, D.G.: On Linear Programming, Integer Programming and Cutting Planes. Ph.D. thesis, Georgia Institute of Technology (2006)"},{"issue":"6","key":"14_CR13","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1016\/j.orl.2006.12.010","volume":"35","author":"DL Applegate","year":"2007","unstructured":"Applegate, D.L., Cook, W., Dash, S., Espinoza, D.G.: Exact solutions to linear programming problems. Oper. Res. Lett. 35(6), 693\u2013699 (2007)","journal-title":"Oper. Res. Lett."},{"key":"14_CR14","unstructured":"Steffensen, J.L.: QSopt\n                      \n                        \n                      \n                      $$\\_$$\n                    ex - an exact linear programming solver (2014)"},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1016\/j.econlet.2016.01.028","volume":"141","author":"F Brandl","year":"2016","unstructured":"Brandl, F., Brandt, F., Suksompong, W.: The impossibility of extending random dictatorship to weak preferences. Econ. Lett. 141, 44\u201347 (2016)","journal-title":"Econ. Lett."},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1016\/j.econlet.2016.01.028","volume":"141","author":"F Brandl","year":"2016","unstructured":"Brandl, F., Brandt, F., Suksompong, W.: Corrigendum to the impossibility of extending random dictatorship to weak preferences. Econ. Lett. 141, 44\u201347 (2016)","journal-title":"Econ. Lett."},{"key":"14_CR17","unstructured":"Geist, C., Peters, D.: Computer-aided methods for social choice theory. In: Endriss, U. (ed.) Trends in Computational Social Choice, pp. 249\u2013267, AI Access (2017)"},{"key":"14_CR18","unstructured":"Nipkow, T.: Arrow and Gibbard-Satterthwaite. Archive of formal proofs formal proof development, September 2008. \n                      http:\/\/isa-afp.org\/entries\/ArrowImpossibilityGS.html"},{"issue":"3","key":"14_CR19","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s10817-009-9147-4","volume":"43","author":"T Nipkow","year":"2009","unstructured":"Nipkow, T.: Social choice theory in HOL. J. Autom. Reasoning 43(3), 289\u2013304 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR20","unstructured":"Gammie, P.: Some classical results in social choice theory. Archive of Formal Proofs, formal proof development, November 2008. \n                      http:\/\/isa-afp.org\/entries\/SenSocialChoice.html"},{"key":"14_CR21","unstructured":"Gammie, P.: Stable matching. Archive of Formal Proofs, formal proof development, October 2016. \n                      http:\/\/isa-afp.org\/entries\/Stable_Matching.html"},{"issue":"1","key":"14_CR22","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s12046-009-0005-1","volume":"34","author":"F Wiedijk","year":"2009","unstructured":"Wiedijk, F.: Formalizing arrow\u2019s theorem. Sadhana 34(1), 193\u2013220 (2009)","journal-title":"Sadhana"},{"key":"14_CR23","unstructured":"Brandt, F., Saile, C., Stricker, C.: Voting with ties: strong impossibilities via sat solving. In: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Richland, SC, International Foundation for Autonomous Agents and Multiagent Systems, pp. 1285\u20131293 (2018)"},{"key":"14_CR24","unstructured":"Brandt, F., Eberl, M., Saile, C., Stricker, C.: The incompatibility of Fishburn-strategyproofness and Pareto-efficiency. Archive of Formal Proofs, formal proof development, March 2018. \n                      http:\/\/isa-afp.org\/entries\/Fishburn_Impossibility.html"},{"key":"14_CR25","unstructured":"Brandl, F., Brandt, F., Geist, C.: Proving the incompatibility of efficiency and strategyproofness via SMT solving. In: Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI) (2016)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29007-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T19:12:58Z","timestamp":1566414778000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-29007-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030290061","9783030290078"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29007-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.frocos2019.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}