{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T13:10:53Z","timestamp":1743081053272,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030294359"},{"type":"electronic","value":"9783030294366"}],"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-29436-6_1","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"1-17","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Unification Modulo Lists with Reverse Relation with Certain Word Equations"],"prefix":"10.1007","author":[{"given":"Siva","family":"Anantharaman","sequence":"first","affiliation":[]},{"given":"Peter","family":"Hibbs","sequence":"additional","affiliation":[]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Rusinowitch","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"key":"1_CR1","unstructured":"Anantharaman, S., Hibbs, P., Narendran, P., Rusinowitch, M.: Unification of lists with reverse as solving simple sets of word equations. Research-Report. https:\/\/hal.archives-ouvertes.fr\/hal-02123648"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-319-08867-9_10","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2014","unstructured":"Abdulla, P.A., et al.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_10"},{"issue":"1","key":"1_CR3","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A Armando","year":"2009","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4:1\u20134:51 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"1_CR4","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1999","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)"},{"issue":"2","key":"1_CR5","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: combining decision procedures. J. Symb. Comput. 21(2), 211\u2013243 (1996)","journal-title":"J. Symb. Comput."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445\u2013532. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"issue":"7","key":"1_CR7","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/79204.79210","volume":"33","author":"A Colmerauer","year":"1990","unstructured":"Colmerauer, A.: An introduction to Prolog III. Commun. ACM 33(7), 69\u201390 (1990)","journal-title":"Commun. ACM"},{"issue":"4","key":"1_CR8","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1007\/s00453-009-9375-3","volume":"60","author":"R Dabrowski","year":"2011","unstructured":"Dabrowski, R., Plandowski, W.: On word equations in one variable. Algorithmica 60(4), 819\u2013828 (2011)","journal-title":"Algorithmica"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/j.ic.2016.09.009","volume":"251","author":"V Diekert","year":"2016","unstructured":"Diekert, V., Jez, A., Plandowski, W.: Finding all solutions of equations in free groups and monoids with involution. Inf. Comput. 251, 263\u2013286 (2016)","journal-title":"Inf. Comput."},{"issue":"12","key":"1_CR10","doi-asserted-by":"publisher","first-page":"1048","DOI":"10.1145\/359657.359666","volume":"21","author":"JV Guttag","year":"1978","unstructured":"Guttag, J.V., Horowitz, E., Musser, D.R.: Abstract data types and software validation. Commun. ACM 21(12), 1048\u20131064 (1978)","journal-title":"Commun. ACM"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-39611-3_21","volume-title":"Hardware and Software: Verification and Testing","author":"V Ganesh","year":"2013","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what\u2019s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209\u2013226. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_21"},{"key":"1_CR12","unstructured":"Hibbs, P.: Unification modulo common list functions. Doctoral Dissertation. University at Albany\u2013SUNY (2015)"},{"key":"1_CR13","unstructured":"Kapur, D.: Towards a theory for abstract data types. Doctoral Dissertation. Massachusetts Institute of Technology (1980)"},{"issue":"2","key":"1_CR14","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D Kapur","year":"1987","unstructured":"Kapur, D., Musser, D.R.: Proof by consistency. Artif. Intell. 31(2), 125\u2013157 (1987)","journal-title":"Artif. Intell."},{"key":"1_CR15","first-page":"12","volume-title":"Combinatorics on Words: A New Challenging Topic","author":"J Karhum\u00e4ki","year":"2004","unstructured":"Karhum\u00e4ki, J.: Combinatorics on Words: A New Challenging Topic, p. 12. Turku Centre for Computer Science, Turku (2004)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-24246-0_9","volume-title":"Frontiers of Combining Systems","author":"T Liang","year":"2015","unstructured":"Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C.: A decision procedure for regular membership and length constraints over unbounded strings. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS, vol. 9322, pp. 135\u2013150. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_9"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Lin, A.W., Majumdar, R.: Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility. arXiv preprint arXiv:1805.06701 (2018)","DOI":"10.1007\/978-3-030-01090-4_21"},{"issue":"2","key":"1_CR18","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/S0304-3975(96)00081-3","volume":"168","author":"K Morita","year":"1996","unstructured":"Morita, K.: Universality of a reversible two-counter machine. Theoret. Comput. Sci. 168(2), 303\u2013320 (1996)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"1_CR19","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/TSE.1980.230459","volume":"6","author":"DR Musser","year":"1980","unstructured":"Musser, D.R.: Abstract data type specification in the AFFIRM system. IEEE Trans. Softw. Eng. 6(1), 24\u201332 (1980)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Musser, D.R.: On proving inductive properties of abstract data types. In: Proceedings of the Seventh Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 154\u2013162 (1980)","DOI":"10.1145\/567446.567461"},{"issue":"2","key":"1_CR21","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"1_CR22","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/322203.322204","volume":"27","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. J. ACM 27(3), 403\u2013411 (1980)","journal-title":"J. ACM"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Plandowski, W.: An efficient algorithm for solving word equations. In: Proceedings of the ACM Symposium on the Theory of Computing, pp. 467\u2013476 (2006)","DOI":"10.1145\/1132516.1132584"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-49116-3_20","volume-title":"STACS 99","author":"JM Robson","year":"1999","unstructured":"Robson, J.M., Diekert, V.: On quadratic word equations. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 217\u2013226. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49116-3_20"},{"issue":"1","key":"1_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"RE Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1\u201312 (1984)","journal-title":"J. ACM"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/BFb0022264","volume-title":"Computer Science Logic","author":"KU Schulz","year":"1995","unstructured":"Schulz, K.U.: On existential theories of list concatenation. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 294\u2013308. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0022264"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 27"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:53:21Z","timestamp":1657576401000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_1","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":"20 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Natal","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":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.mat.ufrn.br\/CADE-27\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}