{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T00:22:25Z","timestamp":1758673345693,"version":"3.44.0"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T00:00:00Z","timestamp":1752192000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T00:00:00Z","timestamp":1752192000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000275","name":"Leverhulme Trust","doi-asserted-by":"publisher","award":["RPG-2019-313","RPG-2019-313"],"award-info":[{"award-number":["RPG-2019-313","RPG-2019-313"]}],"id":[{"id":"10.13039\/501100000275","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We demonstrate how a generic automated theorem prover can be applied to establish the non-orderability of groups. Our approach incorporates various tools such as reasoning from the first principles, positive cones, torsions, generalised torsions and cofinal elements.<\/jats:p>","DOI":"10.1007\/s10817-025-09734-9","type":"journal-article","created":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T13:36:44Z","timestamp":1752241004000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated reasoning for proving non-orderability of groups"],"prefix":"10.1007","volume":"69","author":[{"given":"Alexei","family":"Lisitsa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zipei","family":"Nie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexei","family":"Vernitski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,11]]},"reference":[{"unstructured":"Kokorin, A.\u00a0I., Kopytov, V.\u00a0M.: Fully ordered groups (J. Wiley, 1974)","key":"9734_CR1"},{"unstructured":"Mura, R.\u00a0B., Rhemtulla, A.: Orderable groups (M. Dekker, 1977)","key":"9734_CR2"},{"unstructured":"Kopytov, V.\u00a0M., Medvedev, N.\u00a0Y.: Right-ordered groups (Springer Science & Business Media, 1996)","key":"9734_CR3"},{"doi-asserted-by":"crossref","unstructured":"Glass, A. M.\u00a0W.: Partially ordered groups Vol.\u00a07 (World Scientific, 1999)","key":"9734_CR4","DOI":"10.1142\/3811"},{"unstructured":"Baumslag, G., Charles\u00a0III, F.: Algorithms and classification in combinatorial group theory Vol.\u00a023 (Springer Science & Business Media, 2012)","key":"9734_CR5"},{"key":"9734_CR6","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1090\/S0002-9947-1994-1214782-4","volume":"345","author":"P Dehornoy","year":"1994","unstructured":"Dehornoy, P.: Braid groups and left distributive operations. Transactions of the American Mathematical Society 345, 115\u2013150 (1994)","journal-title":"Transactions of the American Mathematical Society"},{"unstructured":"Short, H., Wiest, B.: Orderings of mapping class groups after thurston. arXiv preprint math\/9907104 (1999)","key":"9734_CR7"},{"key":"9734_CR8","doi-asserted-by":"publisher","first-page":"837","DOI":"10.1142\/S0218216598000425","volume":"7","author":"D Rolfsen","year":"1998","unstructured":"Rolfsen, D., Zhu, J.: Braids, orderings and zero divisors. Journal of Knot Theory and Its Ramifications 7, 837\u2013841 (1998)","journal-title":"Journal of Knot Theory and Its Ramifications"},{"key":"9734_CR9","doi-asserted-by":"publisher","first-page":"209","DOI":"10.2140\/pjm.2000.194.209","volume":"194","author":"C Rourke","year":"2000","unstructured":"Rourke, C., Wiest, B.: Order automatic mapping class groups. Pacific Journal of Mathematics 194, 209\u2013227 (2000)","journal-title":"Pacific Journal of Mathematics"},{"key":"9734_CR10","doi-asserted-by":"publisher","first-page":"657","DOI":"10.4007\/annals.2019.190.2.5","volume":"190","author":"J Hyde","year":"2019","unstructured":"Hyde, J.: The group of boundary fixing homeomorphisms of the disc is not left-orderable. Annals of Mathematics 190, 657\u2013661 (2019)","journal-title":"Annals of Mathematics"},{"key":"9734_CR11","doi-asserted-by":"publisher","first-page":"243","DOI":"10.5802\/aif.2098","volume":"55","author":"S Boyer","year":"2005","unstructured":"Boyer, S., Rolfsen, D., Wiest, B.: Orderable 3-manifold groups. Annales de l\u2019institut Fourier 55, 243\u2013288 (2005)","journal-title":"Annales de l\u2019institut Fourier"},{"key":"9734_CR12","doi-asserted-by":"publisher","first-page":"1213","DOI":"10.1007\/s00208-012-0852-7","volume":"356","author":"S Boyer","year":"2013","unstructured":"Boyer, S., Gordon, C.M., Watson, L.: On L-spaces and left-orderable fundamental groups. Mathematische Annalen 356, 1213\u20131245 (2013)","journal-title":"Mathematische Annalen"},{"doi-asserted-by":"crossref","unstructured":"Juh\u00e1sz, A., Manturov, V.\u00a0O., Kauffman, L.\u00a0H.: (eds) A survey of Heegaard Floer homology. (eds Manturov, V.\u00a0O. & Kauffman, L.\u00a0H.) New ideas in low dimensional topology, 237\u2013296 (World Scientific, 2015)","key":"9734_CR13","DOI":"10.1142\/9789814630627_0007"},{"unstructured":"Ito, T.: Alexander polynomial obstruction of bi-orderability for rationally homologically fibered knot groups. arXiv preprint arXiv:1609.03673 (2016)","key":"9734_CR14"},{"key":"9734_CR15","first-page":"333","volume":"122","author":"D Witte","year":"1994","unstructured":"Witte, D.: Arithmetic groups of higher $$\\mathbb{Q} $$-rank cannot act on $$1$$-manifolds. Proceedings of the American Mathematical Society 122, 333\u2013340 (1994)","journal-title":"Proceedings of the American Mathematical Society"},{"key":"9734_CR16","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s00222-002-0271-6","volume":"152","author":"D Calegari","year":"2003","unstructured":"Calegari, D., Dunfield, N.M.: Laminations and groups of homeomorphisms of the circle. Inventiones mathematicae 152, 149\u2013204 (2003)","journal-title":"Inventiones mathematicae"},{"key":"9734_CR17","doi-asserted-by":"publisher","first-page":"2075","DOI":"10.2140\/gt.2020.24.2075","volume":"24","author":"NM Dunfield","year":"2020","unstructured":"Dunfield, N.M.: Floer homology, group orderability, and taut foliations of hyperbolic $$3$$-manifolds. Geometry & Topology 24, 2075\u20132125 (2020)","journal-title":"Geometry & Topology"},{"key":"9734_CR18","doi-asserted-by":"publisher","first-page":"409","DOI":"10.4171\/lem\/66-3\/4-5","volume":"66","author":"M Triestino","year":"2021","unstructured":"Triestino, M.: On James Hyde\u2019s example of non-orderable subgroup of $$\\rm Homeo (d,\\partial d)$$. L\u2019Enseignement Math\u00e9matique 66, 409\u2013418 (2021)","journal-title":"L\u2019Enseignement Math\u00e9matique"},{"unstructured":"Antol\u0131n, Y., Dicks, W., Sunic, Z., Broaddus, N., Davis, M., Lafont, J.\u00a0F., Ortiz, I.\u00a0J.: (eds) Left relatively convex subgroups. (eds Broaddus, N., Davis, M., Lafont, J.\u00a0F. & Ortiz, I.\u00a0J.) Topological Methods in Group Theory (London Mathematical Society Lecture Note Series), 1\u201318 (Cambridge University Press, 2018)","key":"9734_CR19"},{"doi-asserted-by":"crossref","unstructured":"Clay, A.\u00a0J.: The space of left orderings of a group with applications to topology. Ph.D. thesis, University of British Columbia (2010)","key":"9734_CR20","DOI":"10.4171\/ggd\/93"},{"unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/","key":"9734_CR21"},{"key":"9734_CR22","doi-asserted-by":"publisher","first-page":"885","DOI":"10.1007\/s00233-021-10185-y","volume":"102","author":"F Wehrung","year":"2021","unstructured":"Wehrung, F.: Right-orderability versus left-orderability for monoids. Semigroup Forum 102, 885\u2013899 (2021)","journal-title":"Semigroup Forum"},{"key":"9734_CR23","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1023\/A:1023346206070","volume":"42","author":"VG Bardakov","year":"2003","unstructured":"Bardakov, V.G., Vesnin, A.Y.: A generalization of fibonacci groups. Algebra and Logic 42, 73\u201391 (2003)","journal-title":"Algebra and Logic"},{"key":"9734_CR24","first-page":"169","volume":"90","author":"HM Hilden","year":"1992","unstructured":"Hilden, H.M., Lozano, M.T., Montesinos-Amilibia, J.M.: The arithmeticity of the figure eight knot orbifolds. Topology 90, 169\u2013183 (1992)","journal-title":"Topology"},{"key":"9734_CR25","doi-asserted-by":"publisher","first-page":"32","DOI":"10.4153\/CMB-2005-003-6","volume":"48","author":"MK D\u0105bkowski","year":"2005","unstructured":"D\u0105bkowski, M.K., Przytycki, J.H., Togha, A.A.: Non-left-orderable 3-manifold groups. Canadian Mathematical Bulletin 48, 32\u201340 (2005)","journal-title":"Canadian Mathematical Bulletin"},{"key":"9734_CR26","doi-asserted-by":"publisher","first-page":"1511","DOI":"10.1080\/00927879808826218","volume":"26","author":"CP Chalk","year":"1998","unstructured":"Chalk, C.P.: Fibonacci groups with aspherical presentations. Communications in Algebra 26, 1511\u20131546 (1998)","journal-title":"Communications in Algebra"},{"doi-asserted-by":"crossref","unstructured":"Ba, I., Elhamdadi, M.: Knot groups, quandle extensions and orderability. arXiv preprint arXiv:2307.08605 (2023)","key":"9734_CR27","DOI":"10.1007\/s10711-023-00876-x"},{"key":"9734_CR28","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/BF00966376","volume":"17","author":"S Zheleva","year":"1976","unstructured":"Zheleva, S.: Cyclically ordered groups. Siberian Mathematical Journal 17, 773\u2013777 (1976)","journal-title":"Siberian Mathematical Journal"},{"key":"9734_CR29","doi-asserted-by":"publisher","first-page":"896","DOI":"10.1016\/j.apal.2018.04.007","volume":"169","author":"M Giraudet","year":"2018","unstructured":"Giraudet, M., Leloup, G., Lucas, F.: First order theory of cyclically ordered groups. Annals of Pure and Applied Logic 169, 896\u2013927 (2018)","journal-title":"Annals of Pure and Applied Logic"},{"doi-asserted-by":"crossref","unstructured":"Chiswell, I.\u00a0M., Glass, A.\u00a0M., Wilson, J.\u00a0S. Green, B.\u00a0J.: (ed.) Residual nilpotence and ordering in one-relator groups and knot groups. (ed.Green, B.\u00a0J.) Mathematical Proceedings of the Cambridge Philosophical Society, Vol. 158, 275\u2013288 (Cambridge University Press, 2015)","key":"9734_CR30","DOI":"10.1017\/S0305004114000644"},{"key":"9734_CR31","doi-asserted-by":"publisher","first-page":"182","DOI":"10.4153\/CMB-2015-004-4","volume":"59","author":"G Naylor","year":"2016","unstructured":"Naylor, G., Rolfsen, D.: Generalized torsion in knot groups. Canadian Mathematical Bulletin 59, 182\u2013189 (2016)","journal-title":"Canadian Mathematical Bulletin"},{"key":"9734_CR32","first-page":"1","volume":"30","author":"T Chinburg","year":"2001","unstructured":"Chinburg, T., Friedman, E., Jones, K.N., Reid, A.W.: The arithmetic hyperbolic $$3 $$-manifold of smallest volume. Annali della Scuola Normale Superiore di Pisa-Classe di Scienze 30, 1\u201340 (2001)","journal-title":"Annali della Scuola Normale Superiore di Pisa-Classe di Scienze"},{"doi-asserted-by":"crossref","unstructured":"Clay, A., Rolfsen, D.: Ordered groups and topology Vol. 176 (American Mathematical Soc., 2016)","key":"9734_CR33","DOI":"10.1090\/gsm\/176"},{"key":"9734_CR34","doi-asserted-by":"publisher","first-page":"830","DOI":"10.4153\/CMB-2017-008-8","volume":"60","author":"K Motegi","year":"2017","unstructured":"Motegi, K., Teragaito, M.: Generalized torsion elements and bi-orderability of $$3$$-manifold groups. Canadian Mathematical Bulletin 60, 830\u2013844 (2017)","journal-title":"Canadian Mathematical Bulletin"},{"key":"9734_CR35","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1142\/S1793525320500053","volume":"13","author":"Y Antol\u00edn","year":"2021","unstructured":"Antol\u00edn, Y., Rivas, C.: The space of relative orders and a generalization of Morris indicability theorem. Journal of Topology and Analysis 13, 75\u201385 (2021)","journal-title":"Journal of Topology and Analysis"},{"key":"9734_CR36","doi-asserted-by":"publisher","first-page":"22","DOI":"10.4153\/CMB-1993-004-2","volume":"36","author":"IM Chiswell","year":"1993","unstructured":"Chiswell, I.M., Kropholler, P.H.: Soluble right orderable groups are locally indicable. Canadian Mathematical Bulletin 36, 22\u201329 (1993)","journal-title":"Canadian Mathematical Bulletin"},{"key":"9734_CR37","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1090\/S0002-9939-99-05534-3","volume":"128","author":"P Longobardi","year":"2000","unstructured":"Longobardi, P., Maj, M., Rhemtulla, A.: When is a right orderable group locally indicable? Proceedings of the American Mathematical Society 128, 637\u2013641 (2000)","journal-title":"Proceedings of the American Mathematical Society"},{"unstructured":"Boyer, S., Clay, A.: Order-detection of slopes on the boundaries of knot manifolds. arXiv preprint arXiv:2206.00848 (2022)","key":"9734_CR38"},{"key":"9734_CR39","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1307\/mmj\/1028998233","volume":"6","author":"P Conrad","year":"1959","unstructured":"Conrad, P.: Right-ordered groups. Michigan Mathematical Journal 6, 267\u2013275 (1959)","journal-title":"Michigan Mathematical Journal"},{"key":"9734_CR40","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/j.aim.2017.01.026","volume":"310","author":"S Boyer","year":"2017","unstructured":"Boyer, S., Clay, A.: Foliations, orders, representations, L-spaces and graph manifolds. Advances in Mathematics 310, 159\u2013234 (2017)","journal-title":"Advances in Mathematics"},{"unstructured":"Nie, Z.: On $$1$$-bridge braids, satellite knots, the manifold $$v2503$$ and non-left-orderable surgeries and fillings. arXiv preprint arXiv:2003.14296 (2020)","key":"9734_CR41"},{"key":"9734_CR42","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1007\/s40306-014-0091-y","volume":"39","author":"C Gordon","year":"2014","unstructured":"Gordon, C., Lidman, T.: Taut foliations, left-orderability, and cyclic branched covers. Acta Mathematica Vietnamica 39, 599\u2013635 (2014)","journal-title":"Acta Mathematica Vietnamica"},{"doi-asserted-by":"publisher","unstructured":"Lisitsa, A., Nie, Z., Vernitski, A.: Code and data for the paper Automated reasoning for proving non-orderability of groups (2023). https:\/\/doi.org\/10.5281\/zenodo.8422478","key":"9734_CR43","DOI":"10.5281\/zenodo.8422478"},{"unstructured":"Akhmedov, A., Martin, C.: Non-bi-orderability of $$6_2$$ and $$7_6$$. arXiv preprint arXiv: 1512.00372 (2017)","key":"9734_CR44"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09734-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09734-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09734-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:02:56Z","timestamp":1758664976000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09734-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,11]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["9734"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09734-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,7,11]]},"assertion":[{"value":"27 March 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 June 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 July 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"19"}}