{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T07:25:04Z","timestamp":1785223504233,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662576687","type":"print"},{"value":"9783662576694","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-662-57669-4_10","type":"book-chapter","created":{"date-parts":[[2018,6,26]],"date-time":"2018-06-26T08:48:51Z","timestamp":1530002931000},"page":"179-195","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Unification Modulo Builtins"],"prefix":"10.1007","author":[{"given":"\u015etefan","family":"Ciob\u00e2c\u0103","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Arusoaie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dorel","family":"Lucanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,6,27]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Aguirre, L., Mart\u00ed-Oliet, N., Palomino, M., Pita, I.: Conditional narrowing modulo SMT and axioms. In: PPDP, pp. 17\u201328 (2017)","DOI":"10.1145\/3131851.3131856"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-319-02654-1_16","volume-title":"Software Language Engineering","author":"A Arusoaie","year":"2013","unstructured":"Arusoaie, A., Lucanu, D., Rusu, V.: A generic framework for symbolic execution. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 281\u2013301. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02654-1_16"},{"key":"10_CR3","first-page":"48","volume":"44","author":"A Arusoaie","year":"2015","unstructured":"Arusoaie, A., Lucanu, D., Rusu, V.: Symbolic execution based on language transformation. Comput. Lang. Syst. Struct. 44, 48\u201371 (2015)","journal-title":"Comput. Lang. Syst. Struct."},{"issue":"2","key":"10_CR4","first-page":"211","volume":"21","author":"F Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: combining decision procedures. JSC 21(2), 211\u2013243 (1996)","journal-title":"JSC"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-319-68034-7_5","volume-title":"Formal Aspects of Component Software","author":"K Bae","year":"2017","unstructured":"Bae, K., Rocha, C.: Guarded terms for rewriting modulo SMT. In: Proen\u00e7a, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 78\u201397. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68034-7_5"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Ciob\u00e2c\u0103, \u015e., Lucanu, D.: A coinductive approach to proving reachability properties in logically constrained term rewriting systems. IJCAR (2018, to appear)","DOI":"10.1007\/978-3-319-94205-6_20"},{"key":"10_CR7","unstructured":"Ciob\u00e2c\u0103, \u015e., Lucanu, D.: RMT: proving reachability properties in constrained term rewriting systems modulo theories. Technical report TR 16\u201301, Alexandru Ioan Cuza University, Faculty of Computer Science (2016)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-319-08918-8_29","volume-title":"Rewriting and Typed Lambda Calculi","author":"A \u015etef\u0103nescu","year":"2014","unstructured":"\u015etef\u0103nescu, A., Ciob\u00e2c\u0103, \u015e., Mereuta, R., Moore, B.M., \u015eerb\u0103nut\u0103, T.F., Ro\u015fu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 425\u2013440. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_29"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/3-540-54317-1_111","volume-title":"Conditional and Typed Rewriting Systems","author":"J Darlington","year":"1991","unstructured":"Darlington, J., Guo, Y.: Constrained equational deduction. In: Kaplan, S., Okada, M. (eds.) CTRS 1990. LNCS, vol. 516, pp. 424\u2013435. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54317-1_111"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-70590-1_7","volume-title":"Rewriting Techniques and Applications","author":"S Falke","year":"2008","unstructured":"Falke, S., Kapur, D.: Dependency pairs for rewriting with built-in numbers and semantic data structures. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 94\u2013109. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70590-1_7"},{"issue":"2","key":"10_CR11","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/3060143","volume":"18","author":"C Fuhs","year":"2017","unstructured":"Fuhs, C., Kop, C., Nishida, N.: Verifying procedural programs via constrained rewriting induction. ACM TOCL 18(2), 14:1\u201314:50 (2017)","journal-title":"ACM TOCL"},{"key":"10_CR12","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Research report RR-1358, INRIA (1990). Projet EURECA"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-40885-4_24","volume-title":"Frontiers of Combining Systems","author":"C Kop","year":"2013","unstructured":"Kop, C., Nishida, N.: Term rewriting with logical constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 343\u2013358. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_24"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-319-23165-5_21","volume-title":"Logic, Rewriting, and Concurrency","author":"D Lucanu","year":"2015","unstructured":"Lucanu, D., Rusu, V., Arusoaie, A., Nowak, D.: Verifying reachability-logic properties on rewriting-logic specifications. In: Mart\u00ed-Oliet, N., \u00d6lveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 451\u2013474. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23165-5_21"},{"issue":"2","key":"10_CR15","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 TOPLAS 1(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-319-45741-3_23","volume-title":"Computer Security \u2013 ESORICS 2016","author":"V Nigam","year":"2016","unstructured":"Nigam, V., Talcott, C., Aires Urquiza, A.: Towards the automated verification of cyber-physical security protocols: bounding the number of timed intruders. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 450\u2013470. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45741-3_23"},{"issue":"1","key":"10_CR17","first-page":"269","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. JLAMP 86(1), 269\u2013297 (2017)","journal-title":"JLAMP"},{"issue":"4","key":"10_CR18","first-page":"1","volume":"13","author":"G Ro\u015fu","year":"2017","unstructured":"Ro\u015fu, G.: Matching logic. LMCS 13(4), 1\u201361 (2017)","journal-title":"LMCS"},{"issue":"1","key":"10_CR19","first-page":"51","volume":"8","author":"M Schmidt-Schauss","year":"1989","unstructured":"Schmidt-Schauss, M.: Unification in a combination of arbitrary disjoint equational theories. JSC 8(1), 51\u201399 (1989)","journal-title":"JSC"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Skeirik, S., \u015etef\u0103nescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. CoRR, abs\/1709.05045 (2017)","DOI":"10.1007\/978-3-319-94460-9_12"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-57669-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T00:09:25Z","timestamp":1571530165000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-57669-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783662576687","9783662576694"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-57669-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}