{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:28:44Z","timestamp":1743118124908,"version":"3.40.3"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319587400"},{"type":"electronic","value":"9783319587417"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-58741-7_3","type":"book-chapter","created":{"date-parts":[[2017,5,11]],"date-time":"2017-05-11T12:59:28Z","timestamp":1494507568000},"page":"24-31","source":"Crossref","is-referenced-by-count":1,"title":["Formalizing a Fragment of Combinatorics on Words"],"prefix":"10.1007","author":[{"given":"\u0160t\u011bp\u00e1n","family":"Holub","sequence":"first","affiliation":[]},{"given":"Robert","family":"Veroff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,12]]},"reference":[{"key":"3_CR1","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C-L Chang","year":"1973","unstructured":"Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York (1973)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Culik II, K., Karhum\u00e4ki, J.: On the equality sets for homomorphisms on free monoids with two generators. RAIRO ITA 14(4), 349\u2013369 (1980)","DOI":"10.1051\/ita\/1980140403491"},{"issue":"6","key":"3_CR3","doi-asserted-by":"crossref","first-page":"1167","DOI":"10.1142\/S0129054107005212","volume":"18","author":"E Czeizler","year":"2007","unstructured":"Czeizler, E., Holub, \u0160., Karhum\u00e4ki, J., Laine, M.: Intricacies of simple word equations: An example. Int. J. Found. Comput. Sci. 18(6), 1167\u20131175 (2007)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"1","key":"3_CR4","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1090\/S0002-9939-1965-0174934-9","volume":"16","author":"NJ Fine","year":"1965","unstructured":"Fine, N.J., Wilf, H.S.: Uniqueness theorems for periodic functions. Proc. Am. Math. Soc. 16(1), 109\u2013109 (1965)","journal-title":"Proc. Am. Math. Soc."},{"key":"3_CR5","unstructured":"Hadravov\u00e1, J.: Structure of equality sets. Ph.D. thesis, Charles University (2007)"},{"issue":"11","key":"3_CR6","first-page":"1370","volume":"55","author":"TC Hales","year":"2008","unstructured":"Hales, T.C.: Formal proof. Not. AMS 55(11), 1370\u20131380 (2008)","journal-title":"Not. AMS"},{"issue":"1","key":"3_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0021-8693(02)00534-3","volume":"259","author":"\u0160 Holub","year":"2003","unstructured":"Holub, \u0160.: Binary equality sets are generated by two words. J. Algebra 259(1), 1\u201342 (2003)","journal-title":"J. Algebra"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/3-540-45005-X_21","volume-title":"Developments in Language Theory","author":"\u0160 Holub","year":"2003","unstructured":"Holub, \u0160.: A unique structure of two-generated binary equality sets. In: Ito, M., Toyama, M. (eds.) DLT 2002. LNCS, vol. 2450, pp. 245\u2013257. Springer, Heidelberg (2003). doi:\n10.1007\/3-540-45005-X_21"},{"key":"3_CR9","unstructured":"Holub, \u0160., Veroff, R.: Formalizing a fragment of combinatorics on words (web support) (2017). \nhttp:\/\/www.cs.unm.edu\/veroff\/CiE2017\/"},{"key":"3_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4614-1129-1","volume-title":"The Kepler Conjecture: The Hales-Ferguson Proof","author":"JC Lagarias","year":"2011","unstructured":"Lagarias, J.C.: The Kepler Conjecture: The Hales-Ferguson Proof. Springer, New York (2011)"},{"key":"3_CR11","first-page":"141","volume":"36","author":"FW Levi","year":"1944","unstructured":"Levi, F.W.: On semigroups. Bull. Calcutta Math. Soc. 36, 141\u2013146 (1944)","journal-title":"Bull. Calcutta Math. Soc."},{"key":"3_CR12","unstructured":"McCune, W.: Prover9, version 02a (2009). \nhttp:\/\/www.cs.unm.edu\/mccune\/prover9\/"},{"key":"3_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195218","volume-title":"Elements of Automata Theory","author":"J Sakarovitch","year":"2009","unstructured":"Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, New York (2009)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-36675-8_13","volume-title":"Automated Reasoning and Mathematics","author":"J Urban","year":"2013","unstructured":"Urban, J., Vysko\u010dil, J.: Theorem proving in large formal mathematics as an emerging AI field. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 240\u2013257. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-36675-8_13"}],"container-title":["Lecture Notes in Computer Science","Unveiling Dynamics and Complexity"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-58741-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,31]],"date-time":"2017-08-31T08:59:24Z","timestamp":1504169964000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-58741-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319587400","9783319587417"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-58741-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}