{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,19]],"date-time":"2025-05-19T13:30:31Z","timestamp":1747661431725,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030887070"},{"type":"electronic","value":"9783030887087"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88708-7_9","type":"book-chapter","created":{"date-parts":[[2021,10,4]],"date-time":"2021-10-04T21:47:06Z","timestamp":1633384026000},"page":"111-127","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Voting Theory in the Lean Theorem Prover"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6054-9052","authenticated-orcid":false,"given":"Wesley H.","family":"Holliday","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8954-3770","authenticated-orcid":false,"given":"Chase","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0751-9011","authenticated-orcid":false,"given":"Eric","family":"Pacuit","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,4]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10458-009-9115-8","volume":"22","author":"T Agotnes","year":"2009","unstructured":"Agotnes, T., van der Hoek, W., Wooldridge, M.: On the logic of preference and judgment aggregation. Auton. Agent. Multi-Agent Syst. 22(1), 4\u201330 (2009)","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"9_CR2","volume-title":"Social Choice and Individual Values","author":"KJ Arrow","year":"1951","unstructured":"Arrow, K.J.: Social Choice and Individual Values, 1st edn. Wiley, New York (1951)","edition":"1"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"143","DOI":"10.7312\/mask15328-008","volume-title":"The Arrow Impossibility Theorem","author":"KJ Arrow","year":"2014","unstructured":"Arrow, K.J.: Origins of the impossibility theorem. In: Maskin, E., Sen, A. (eds.) The Arrow Impossibility Theorem, pp. 143\u2013148. Columbia University Press, New York (2014)"},{"key":"9_CR4","unstructured":"Avigad, J., de Moura, L., Kong, S.: Theorem Proving in Lean. Release 3.23.0 edn. (2021). https:\/\/leanprover.github.io\/theorem_proving_in_lean\/theorem_proving_in_lean.pdf"},{"issue":"4","key":"9_CR5","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/BF01229471","volume":"47","author":"N Baigent","year":"1987","unstructured":"Baigent, N.: Twitching weak dictators. J. Econ. 47(4), 407\u2013411 (1987)","journal-title":"J. Econ."},{"key":"9_CR6","unstructured":"Blau, J.H.: Review of the article \u201cRepairing proofs of arrow\u2019s general impossibility theorem and enlarging the scope of the theorem\u201d by R. Routley. Math. Rev., 0545435 (1979). https:\/\/mathscinet.ams.org\/mathscinet-getitem?mr=545435"},{"issue":"2","key":"9_CR7","doi-asserted-by":"publisher","first-page":"302","DOI":"10.2307\/1910256","volume":"25","author":"JH Blau","year":"1957","unstructured":"Blau, J.H.: The existence of social welfare functions. Econometrica 25(2), 302\u2013313 (1957)","journal-title":"Econometrica"},{"key":"9_CR8","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3125642"},{"key":"9_CR9","unstructured":"Brandt, F., Eberl, M., Saile, C., Stricker, C.: The incompatibility of Fishburn-strategyproofness and Pareto-efficiency. Archive of Formal Proofs (2018). https:\/\/isa-afp.org\/entries\/Fishburn_Impossibility.html"},{"key":"9_CR10","unstructured":"Brandt, F., Saile, C., Stricker, C.: Voting with ties: strong impossibilities via SAT solving. In: Dastani, M., Sukthankar, G., Andr\u00e9, E., Koenig, S. (eds.) Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2018), pp. 1285\u20131293. International Foundation for Autonomous Agents and Multiagent Systems (2018)"},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S0165-1765(99)00209-8","volume":"66","author":"DE Campbell","year":"2000","unstructured":"Campbell, D.E., Kelly, J.S.: Weak independence and veto power. Econ. Lett. 66, 183\u2013189 (2000)","journal-title":"Econ. Lett."},{"issue":"5","key":"9_CR12","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/s10458-016-9328-6","volume":"30","author":"G Cin\u00e1","year":"2016","unstructured":"Cin\u00e1, G., Endriss, U.: Proving classical theorems of social choice theory in modal logic. Auton. Agent. Multi-Agent Syst. 30(5), 963\u2013989 (2016). https:\/\/doi.org\/10.1007\/s10458-016-9328-6","journal-title":"Auton. Agent. Multi-Agent Syst."},{"issue":"2\u20133","key":"9_CR13","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2\u20133), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"9_CR14","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover. In: 25th International Conference on Automated Deduction (CADE-25) (2015)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-030-29007-8_14","volume-title":"Frontiers of Combining Systems","author":"M Eberl","year":"2019","unstructured":"Eberl, M.: Verifying randomised social choice. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 240\u2013256. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_14"},{"key":"9_CR16","first-page":"333","volume-title":"Logic and Philosophy Today","author":"U Endriss","year":"2011","unstructured":"Endriss, U.: Logic and social choice theory. In: Gupta, A., van Benthem, J. (eds.) Logic and Philosophy Today, pp. 333\u2013377. College Publications, London (2011)"},{"issue":"3","key":"9_CR17","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1137\/0133030","volume":"33","author":"PC Fishburn","year":"1977","unstructured":"Fishburn, P.C.: Condorcet social choice functions. SIAM J. Appl. Math. 33(3), 469\u2013489 (1977)","journal-title":"SIAM J. Appl. Math."},{"key":"9_CR18","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511492303","volume-title":"Domain Conditions in Social Choice Theory","author":"W Gaertner","year":"2001","unstructured":"Gaertner, W.: Domain Conditions in Social Choice Theory. Cambridge University Press, Cambridge (2001)"},{"issue":"1","key":"9_CR19","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s00199-004-0556-7","volume":"26","author":"J Geanakoplos","year":"2005","unstructured":"Geanakoplos, J.: Three brief proofs of Arrow\u2019s theorem. Econ. Theor. 26(1), 211\u2013215 (2005)","journal-title":"Econ. Theor."},{"key":"9_CR20","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)"},{"issue":"4","key":"9_CR21","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1007\/s10992-012-9240-8","volume":"42","author":"U Grandi","year":"2013","unstructured":"Grandi, U., Endriss, U.: First-order logic formalisation of impossibility theorems in preference aggregation. J. Philos. Log. 42(4), 595\u2013618 (2013)","journal-title":"J. Philos. Log."},{"key":"9_CR22","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s00355-020-01238-2","volume":"55","author":"WH Holliday","year":"2020","unstructured":"Holliday, W.H., Kelley, M.: A note on Murakami\u2019s theorems and incomplete social choice without the Pareto principle. Soc. Choice Welfare 55, 243\u2013253 (2020)","journal-title":"Soc. Choice Welfare"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s00355-018-1163-z","volume":"54","author":"WH Holliday","year":"2020","unstructured":"Holliday, W.H., Pacuit, E.: Arrow\u2019s decisive coalitions. Soc. Choice Welfare 54, 463\u2013505 (2020)","journal-title":"Soc. Choice Welfare"},{"key":"9_CR24","unstructured":"Holliday, W.H., Pacuit, E.: Split Cycle: a new Condorcet consistent voting method independent of clones and immune to spoilers (2020). arXiv:2004.02350"},{"key":"9_CR25","unstructured":"Holliday, W.H., Pacuit, E.: Stable Voting (2021). arXiv:2108.00542"},{"key":"9_CR26","unstructured":"Holliday, W.H., Pacuit, E.: Axioms for defeat in democratic elections. J. Theoret. Pol. (Forthcoming). arXiv:2008.08451"},{"key":"9_CR27","volume-title":"Intuitionistic Type Theory","author":"P Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis, Napoli (1984)"},{"key":"9_CR28","volume-title":"Logic and Social Choice","author":"Y Murakami","year":"1968","unstructured":"Murakami, Y.: Logic and Social Choice. Dover Publications, New York (1968)"},{"issue":"3","key":"9_CR29","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. Reason. 43(3), 289\u2013304 (2009)","journal-title":"J. Autom. Reason."},{"key":"9_CR30","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-31803-5_11","volume-title":"Dependence Logic","author":"E Pacuit","year":"2016","unstructured":"Pacuit, E., Yang, F.: Dependence and independence in social choice: arrow\u2019s theorem. In: Abramsky, S., Kontinen, J., V\u00e4\u00e4n\u00e4nen, J., Vollmer, H. (eds.) Dependence Logic, pp. 235\u2013260. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-31803-5_11"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Parikh, R.: The logic of games and its applications. In: Karplnski, M., van Leeuwen, J. (eds.) Topics in the Theory of Computation, North-Holland Mathematics Studies, vol. 102, pp. 111\u2013139. North-Holland (1985)","DOI":"10.1016\/S0304-0208(08)73078-0"},{"key":"9_CR32","first-page":"227","volume":"163","author":"M Pauly","year":"2008","unstructured":"Pauly, M.: On the role of language in social choice theory. Soc. Choice Welfare 163, 227\u2013243 (2008)","journal-title":"Soc. Choice Welfare"},{"issue":"4","key":"9_CR33","doi-asserted-by":"publisher","first-page":"879","DOI":"10.1305\/ndjfl\/1093882810","volume":"20","author":"R Routley","year":"1979","unstructured":"Routley, R.: Repairing proofs of Arrow\u2019s general impossibility theorem and enlarging the scope of the theorem. Notre Dame J. Formal Logic 20(4), 879\u2013890 (1979)","journal-title":"Notre Dame J. Formal Logic"},{"issue":"3","key":"9_CR34","doi-asserted-by":"publisher","first-page":"719","DOI":"10.2307\/2526229","volume":"25","author":"A Rubinstein","year":"1984","unstructured":"Rubinstein, A.: The single profile analogues to multi profile theorems: mathematical logic\u2019s approach. Int. Econ. Rev. 25(3), 719\u2013730 (1984)","journal-title":"Int. Econ. Rev."},{"key":"9_CR35","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s00355-010-0475-4","volume":"36","author":"M Schulze","year":"2011","unstructured":"Schulze, M.: A new monotonic, clone-independent, reversal symmetric, and condorcet-consistent single-winner election method. Soc. Choice Welfare 36, 267\u2013303 (2011)","journal-title":"Soc. Choice Welfare"},{"key":"9_CR36","doi-asserted-by":"publisher","DOI":"10.4159\/9780674974616","volume-title":"Collective Choice and Social Welfare: An Expanded Edition","author":"A Sen","year":"2017","unstructured":"Sen, A.: Collective Choice and Social Welfare: An Expanded Edition, Expanded Harvard University Press, Cambridge (2017)","edition":"Expanded"},{"key":"9_CR37","doi-asserted-by":"publisher","first-page":"2010","DOI":"10.1016\/j.artint.2011.07.001","volume":"175","author":"P Tang","year":"2011","unstructured":"Tang, P., Lin, F.: Discovering theorems in game theory: two-person games with unique pure Nash equilibrium payoffs. Artif. Intell. 175, 2010\u20132020 (2011)","journal-title":"Artif. Intell."},{"key":"9_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-77645-3","volume-title":"Mathematics and Politics: Strategy, Voting, Power, and Proof","author":"AD Taylor","year":"2008","unstructured":"Taylor, A.D., Pacelli, A.M.: Mathematics and Politics: Strategy, Voting, Power, and Proof, 2nd edn. Springer, New York (2008). https:\/\/doi.org\/10.1007\/978-0-387-77645-3","edition":"2"},{"key":"9_CR39","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/BF00433944","volume":"4","author":"TN Tideman","year":"1987","unstructured":"Tideman, T.N.: Independence of clones as a criterion for voting rules. Soc. Choice Welfare 4, 185\u2013206 (1987)","journal-title":"Soc. Choice Welfare"},{"issue":"4","key":"9_CR40","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/s10992-011-9189-z","volume":"40","author":"N Troquard","year":"2011","unstructured":"Troquard, N., van der Hoek, W., Wooldridge, M.: Reasoning about social choice functions. J. Philos. Log. 40(4), 473\u2013498 (2011)","journal-title":"J. Philos. Log."},{"issue":"4","key":"9_CR41","doi-asserted-by":"publisher","first-page":"171","DOI":"10.2478\/v10037-007-0020-9","volume":"15","author":"F Wiedijk","year":"2007","unstructured":"Wiedijk, F.: Arrow\u2019s impossibility theorem. Formalized Math. 15(4), 171\u2013174 (2007)","journal-title":"Formalized Math."}],"container-title":["Lecture Notes in Computer Science","Logic, Rationality, and Interaction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88708-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,13]],"date-time":"2021-10-13T18:29:10Z","timestamp":1634149750000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88708-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030887070","9783030887087"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88708-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"4 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LORI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Logic, Rationality and Interaction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Xi\u2019an","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lori2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/golori.org\/lori2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"40","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":"15","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":"7","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":"38% - 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":"2","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":"5","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)"}}]}}