{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:58:03Z","timestamp":1776553083206,"version":"3.51.2"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-07021-0_22","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:43:30Z","timestamp":1759844610000},"page":"392-411","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formalising Fairness in the Assignment Problem with Ordinal Preferences in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Duc Minh","family":"Do","sequence":"first","affiliation":[]},{"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"publisher","unstructured":"Amanatidis, G., Aziz, H., Birmpas, G., Filos-Ratsikas, A., Li, B., Moulin, H., Voudouris, A.A., Wu, X.: Fair division of indivisible goods: Recent progress and open questions. Artif. Intell. 322(C) (Sep 2023). https:\/\/doi.org\/10.1016\/j.artint.2023.103965, https:\/\/doi.org\/10.1016\/j.artint.2023.103965","DOI":"10.1016\/j.artint.2023.103965"},{"key":"22_CR2","unstructured":"Arrow, K.J.: Social Choice and Individual Values. Yale University Press (2012), http:\/\/www.jstor.org\/stable\/j.ctt1nqb90"},{"key":"22_CR3","doi-asserted-by":"publisher","unstructured":"Aziz, H.: Developments in multi-agent fair allocation. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020. pp. 13563\u201313568. AAAI Press (2020). https:\/\/doi.org\/10.1609\/AAAI.V34I09.7082, https:\/\/doi.org\/10.1609\/aaai.v34i09.7082","DOI":"10.1609\/AAAI.V34I09.7082"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Aziz, H., Brandt, F., Elkind, E., Skowron, P.: Computational social choice: The first ten years and beyond. In: Steffen, B., Woeginger, G.J. (eds.) Computing and Software Science - State of the Art and Perspectives, Lecture Notes in Computer Science, vol. 10000, pp. 48\u201365. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_4, https:\/\/doi.org\/10.1007\/978-3-319-91908-9_4","DOI":"10.1007\/978-3-319-91908-9_4"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Aziz, H., Brandt, F., Stursberg, P.: On popular random assignments. In: V\u00f6cking, B. (ed.) Algorithmic Game Theory. pp. 183\u2013194. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-41392-6_16"},{"key":"22_CR6","doi-asserted-by":"publisher","unstructured":"Aziz, H., Gaspers, S., Mackenzie, S., Walsh, T.: Fair assignment of indivisible objects under ordinal preferences. Artificial Intelligence 227, 71\u201392 (2015). https:\/\/doi.org\/10.1016\/j.artint.2015.06.002, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0004370215000880","DOI":"10.1016\/j.artint.2015.06.002"},{"key":"22_CR7","doi-asserted-by":"publisher","unstructured":"Aziz, H., Luo, P., Rizkallah, C.: Incompatibility of efficiency and strategyproofness in the random assignment setting with indifferences. Economics Letters 160, 46\u201349 (2017). https:\/\/doi.org\/10.1016\/j.econlet.2017.08.010, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0165176517303336","DOI":"10.1016\/j.econlet.2017.08.010"},{"key":"22_CR8","doi-asserted-by":"publisher","unstructured":"Aziz, H., Luo, P., Rizkallah, C.: Rank maximal equal contribution: A probabilistic social choice function. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018. pp. 910\u2013916. AAAI Press (2018). https:\/\/doi.org\/10.1609\/AAAI.V32I1.11448, https:\/\/doi.org\/10.1609\/aaai.v32i1.11448","DOI":"10.1609\/AAAI.V32I1.11448"},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Bogomolnaia, A., Moulin, H.: A new solution to the random assignment problem. J. Econ. Theory 100(2), 295\u2013328 (2001). https:\/\/doi.org\/10.1006\/JETH.2000.2710, https:\/\/doi.org\/10.1006\/jeth.2000.2710","DOI":"10.1006\/JETH.2000.2710"},{"key":"22_CR10","doi-asserted-by":"publisher","unstructured":"Bouveret, S., Endriss, U., Lang, J.: Fair division under ordinal preferences: Computing envy-free allocations of indivisible goods. In: Coelho, H., Studer, R., Wooldridge, M.J. (eds.) ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings. Frontiers in Artificial Intelligence and Applications, vol.\u00a0215, pp. 387\u2013392. IOS Press (2010). https:\/\/doi.org\/10.3233\/978-1-60750-606-5-387, https:\/\/doi.org\/10.3233\/978-1-60750-606-5-387","DOI":"10.3233\/978-1-60750-606-5-387"},{"key":"22_CR11","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3125642, https:\/\/doi.org\/10.1145\/3125642","DOI":"10.1145\/3125642"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Brandt, F., Conitzer, V., Endriss, U., Lang, J., Procaccia, A.D.: Handbook of Computational Social Choice. Cambridge University Press, USA, 1st edn. (2016)","DOI":"10.1017\/CBO9781107446984.002"},{"key":"22_CR13","doi-asserted-by":"publisher","unstructured":"Brandt, F., Geist, C.: Finding strategyproof social choice functions via SAT solving. J. Artif. Intell. Res. 55, 565\u2013602 (2016). https:\/\/doi.org\/10.1613\/JAIR.4959, https:\/\/doi.org\/10.1613\/jair.4959","DOI":"10.1613\/JAIR.4959"},{"key":"22_CR14","doi-asserted-by":"publisher","unstructured":"Brandt, F., Geist, C., Peters, D.: Optimal bounds for the no-show paradox via SAT solving. Math. Soc. Sci. 90, 18\u201327 (2017). https:\/\/doi.org\/10.1016\/J.MATHSOCSCI.2016.09.003, https:\/\/doi.org\/10.1016\/j.mathsocsci.2016.09.003","DOI":"10.1016\/J.MATHSOCSCI.2016.09.003"},{"key":"22_CR15","doi-asserted-by":"publisher","unstructured":"Caragiannis, I., Gravin, N., Huang, X.: Envy-freeness up to any item with high nash welfare: The virtue of donating items. In: Karlin, A.R., Immorlica, N., Johari, R. (eds.) Proceedings of the 2019 ACM Conference on Economics and Computation, EC 2019, Phoenix, AZ, USA, June 24-28, 2019. pp. 527\u2013545. ACM (2019). https:\/\/doi.org\/10.1145\/3328526.3329574, https:\/\/doi.org\/10.1145\/3328526.3329574","DOI":"10.1145\/3328526.3329574"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Chakraborty, M., Segal-Halevi, E., Suksompong, W.: Weighted fairness notions for indivisible items revisited. ACM Transactions on Economics and Computation 12(3) (Sep 2024). https:\/\/doi.org\/10.1145\/3665799, https:\/\/doi.org\/10.1145\/3665799","DOI":"10.1145\/3665799"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Do, D.M., Rizkallah, C.: Formalising fairness in the assignment problem with ordinal preferences in isabelle\/hol (artefact), https:\/\/github.com\/crizkallah\/crizkallah.github.io\/blob\/master\/formalisations\/Fairness_Fractional_Assignment.thy, last accessed July 2025","DOI":"10.1007\/978-3-032-07021-0_22"},{"key":"22_CR18","unstructured":"Eberl, M.: Randomised social choice theory. Archive of Formal Proofs (May 2016), https:\/\/isa-afp.org\/entries\/Randomised_Social_Choice.html, Formal proof development"},{"key":"22_CR19","unstructured":"Endriss, U.: Lecture notes on fair division. CoRR abs\/1806.04234 (2018), http:\/\/arxiv.org\/abs\/1806.04234"},{"key":"22_CR20","unstructured":"Gammie, P.: Some classical results in social choice theory. Archive of Formal Proofs (November 2008), https:\/\/isa-afp.org\/entries\/SenSocialChoice.html, Formal proof development"},{"key":"22_CR21","doi-asserted-by":"publisher","unstructured":"Gehrlein, W.V.: Condorcet\u2019s paradox. Theory and Decision 15(2), 161\u2013197 (1983). https:\/\/doi.org\/10.1007\/BF00143070, https:\/\/doi.org\/10.1007\/BF00143070","DOI":"10.1007\/BF00143070"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Gibbard, A.: Manipulation of voting schemes: A general result. Econometrica 41(4), 587\u2013601 (1973), http:\/\/www.jstor.org\/stable\/1914083","DOI":"10.2307\/1914083"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Hall, P.: On representatives of subsets. Classic Papers in Combinatorics pp. 58\u201362 (1987)","DOI":"10.1007\/978-0-8176-4842-8_4"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Halmos, P.R., Vaughan, H.E.: The marriage problem. In: Classic Papers in Combinatorics, pp. 146\u2013147. Springer (2009)","DOI":"10.1007\/978-0-8176-4842-8_11"},{"key":"22_CR25","unstructured":"Jiang, D., Nipkow, T.: Hall\u2019s marriage theorem. Archive of Formal Proofs (December 2010), https:\/\/isa-afp.org\/entries\/Marriage.html, Formal proof development"},{"key":"22_CR26","doi-asserted-by":"publisher","unstructured":"Jiang, D., Nipkow, T.: Proof pearl: The marriage theorem. In: Jouannaud, J., Shao, Z. (eds.) Proceedings of the First International Conference on Certified Programs and Proofs CPP 2011, Kenting, Taiwan, December 7-9, 2011. Lecture Notes in Computer Science, vol.\u00a07086, pp. 394\u2013399. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_28, https:\/\/doi.org\/10.1007\/978-3-642-25379-9_28","DOI":"10.1007\/978-3-642-25379-9_28"},{"key":"22_CR27","doi-asserted-by":"publisher","unstructured":"Li, K.H.: Formalizing May\u2019s theorem. CoRR abs\/2210.05342 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2210.05342, https:\/\/doi.org\/10.48550\/arXiv.2210.05342","DOI":"10.48550\/ARXIV.2210.05342"},{"key":"22_CR28","doi-asserted-by":"publisher","unstructured":"May, K.O.: A set of independent necessary and sufficient conditions for simple majority decision. Econometrica 20(4), 680\u2013684 (1952). https:\/\/doi.org\/10.2307\/1907651","DOI":"10.2307\/1907651"},{"key":"22_CR29","doi-asserted-by":"publisher","unstructured":"Mishra, S., Padala, M., Gujar, S.: Fair allocation of goods and chores - tutorial and survey of recent results. CoRR abs\/2307.10985 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2307.10985, https:\/\/doi.org\/10.48550\/arXiv.2307.10985","DOI":"10.48550\/ARXIV.2307.10985"},{"key":"22_CR30","doi-asserted-by":"crossref","unstructured":"Niculescu, C.P., St\u0103nescu, M.M.: A note on abel\u2019s partial summation formula. Aequationes mathematicae 91, 1009\u20131024 (2017)","DOI":"10.1007\/s00010-017-0504-9"},{"key":"22_CR31","unstructured":"Nipkow, T.: Arrow and Gibbard-Satterthwaite. Archive of Formal Proofs (September 2008), https:\/\/isa-afp.org\/entries\/ArrowImpossibilityGS.html, Formal proof development"},{"key":"22_CR32","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Social choice theory in HOL. Journal of Automated Reasoning 43(3), 289\u2013304 (2009). https:\/\/doi.org\/10.1007\/S10817-009-9147-4, https:\/\/doi.org\/10.1007\/s10817-009-9147-4","DOI":"10.1007\/S10817-009-9147-4"},{"key":"22_CR33","unstructured":"Pacuit, E.: Voting Methods. In: Zalta, E.N., Nodelman, U. (eds.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2024 edn. (2024)"},{"key":"22_CR34","doi-asserted-by":"crossref","unstructured":"Parsert, J., Kaliszyk, C.: Microeconomics and the first welfare theorem. Archive of Formal Proofs (September 2017), https:\/\/isa-afp.org\/entries\/First_Welfare_Theorem.html, Formal proof development","DOI":"10.1145\/3167100"},{"key":"22_CR35","doi-asserted-by":"publisher","unstructured":"Parsert, J., Kaliszyk, C.: Towards formal foundations for game theory. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving (ITP). Lecture Notes in Computer Science, vol. 10895, pp. 495\u2013503. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_29, https:\/\/doi.org\/10.1007\/978-3-319-94821-8_29","DOI":"10.1007\/978-3-319-94821-8_29"},{"key":"22_CR36","unstructured":"Parsert, J., Kaliszyk, C.: Von-neumann-morgenstern utility theorem. Archive of Formal Proofs (July 2018), https:\/\/isa-afp.org\/entries\/Neumann_Morgenstern_Utility.html, Formal proof development"},{"key":"22_CR37","doi-asserted-by":"publisher","unstructured":"Pruhs, K., Woeginger, G.J.: Divorcing made easy. In: Kranakis, E., Krizanc, D., Luccio, F.L. (eds.) Fun with Algorithms - 6th International Conference, FUN 2012, Venice, Italy, June 4-6, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07288, pp. 305\u2013314. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-30347-0_30, https:\/\/doi.org\/10.1007\/978-3-642-30347-0_30","DOI":"10.1007\/978-3-642-30347-0_30"},{"key":"22_CR38","doi-asserted-by":"publisher","unstructured":"Satterthwaite, M.A.: Strategy-proofness and Arrow\u2019s conditions: Existence and correspondence theorems for voting procedures and social welfare functions. Journal of Economic Theory 10(2), 187\u2013217 (1975). https:\/\/doi.org\/10.1016\/0022-0531(75)90050-2, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0022053175900502","DOI":"10.1016\/0022-0531(75)90050-2"},{"key":"22_CR39","doi-asserted-by":"crossref","unstructured":"Satterthwaite, M.A.: Strategy-proofness and arrow\u2019s conditions: Existence and correspondence theorems for voting procedures and social welfare functions. Journal of Economic Theory 10(2), 187\u2013217 (1975). https:\/\/doi.org\/https:\/\/doi.org\/10.1016\/0022-0531(75)90050-2, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0022053175900502","DOI":"10.1016\/0022-0531(75)90050-2"},{"key":"22_CR40","doi-asserted-by":"crossref","unstructured":"Sen, A.K.: The impossibility of a paretian liberal. Journal of Political Economy 78(1), 152\u2013157 (1970)","DOI":"10.1086\/259614"},{"key":"22_CR41","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Formalizing arrow\u2019s theorem. Sadhana 34(1), 193\u2013220 (2009)","DOI":"10.1007\/s12046-009-0005-1"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07021-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:22:12Z","timestamp":1776507732000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032070203","9783032070210"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"8 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brasilia","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2025\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}