{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:18:54Z","timestamp":1725830334297},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242453"},{"type":"electronic","value":"9783319242460"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_15","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"239-255","source":"Crossref","is-referenced-by-count":1,"title":["Formalizing Soundness and Completeness of Unravelings"],"prefix":"10.1007","author":[{"given":"Sarah","family":"Winkler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J., March\u00e9, C., Urbain, X.: Proving termination of membership equational programs. In: Proc. PEPM 2004, pp. 147\u2013158 (2004)","DOI":"10.1145\/1014007.1014022"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-319-08587-6_13","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2014","unstructured":"Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol.\u00a08562, pp. 184\u2013191. Springer, Heidelberg (2014)"},{"key":"15_CR4","unstructured":"Gmeiner, K., Nishida, N., Gramlich, B.: Proving confluence of conditional term rewriting systems via unravelings. In: Proc. IWC 2013, pp. 35\u201339 (2013)"},{"key":"15_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/FI-1995-24121","volume":"24","author":"B. Gramlich","year":"1995","unstructured":"Gramlich, B.: Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae\u00a024, 3\u201323 (1995)","journal-title":"Fundamenta Informaticae"},{"issue":"4","key":"15_CR6","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1016\/j.ipl.2005.05.002","volume":"95","author":"S. Lucas","year":"2005","unstructured":"Lucas, S., March\u00e9, C., Meseguer, J.: Operational termination of conditional term rewriting systems. IPL\u00a095(4), 446\u2013453 (2005)","journal-title":"IPL"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-61735-3_7","volume-title":"Algebraic and Logic Programming","author":"M. Marchiori","year":"1996","unstructured":"Marchiori, M.: Unravelings and ultra-properties. In: Hanus, M., Rodr\u00edguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol.\u00a01139, pp. 107\u2013121. Springer, Heidelberg (1996)"},{"key":"15_CR8","unstructured":"Marchiori, M.: On deterministic conditional rewriting. Technical Report Computation Structures Group Memo 405. MIT (1997)"},{"key":"15_CR9","unstructured":"Nagele, J., Thiemann, R.: Certification of confluence proofs using. In: Proc. 3rd IWC, pp. 19\u201323 (2014)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"15_CR11","unstructured":"Nishida, N.: Transformational Approach to Inverse Computation in Term Rewriting. PhD thesis, Nagoya University (2004)"},{"issue":"3","key":"15_CR12","first-page":"1","volume":"8","author":"N. Nishida","year":"2012","unstructured":"Nishida, N., Sakai, M., Sakabe, T.: Soundness of unravelings for conditional term rewriting systems via ultra-properties related to linearity. LMCS\u00a08(3), 1\u201349 (2012)","journal-title":"LMCS"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-48242-3_8","volume-title":"Logic Programming and Automated Reasoning","author":"E. Ohlebusch","year":"1999","unstructured":"Ohlebusch, E.: Transforming conditional rewrite systems with extra variables into unconditional systems. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol.\u00a01705, pp. 111\u2013130. Springer, Heidelberg (1999)"},{"issue":"1\u20132","key":"15_CR14","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s002000100064","volume":"12","author":"E. Ohlebusch","year":"2001","unstructured":"Ohlebusch, E.: Termination of logic programs: Transformational methods revisited. AAECC\u00a012(1\u20132), 73\u2013116 (2001)","journal-title":"AAECC"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer (2002)","DOI":"10.1007\/978-1-4757-3661-8"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10721975_20","volume-title":"Rewriting Techniques and Applications","author":"E. Ohlebusch","year":"2000","unstructured":"Ohlebusch, E., Claves, C., March\u00e9, C.: TALP: A tool for the termination analysis of logic programs. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 270\u2013273. Springer, Heidelberg (2000)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/978-3-319-08918-8_31","volume-title":"Rewriting and Typed Lambda Calculi","author":"T. Sternagel","year":"2014","unstructured":"Sternagel, T., Middeldorp, A.: Conditional confluence (System description). In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol.\u00a08560, pp. 456\u2013465. Springer, Heidelberg (2014)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 452\u2013468. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,8]],"date-time":"2020-09-08T13:32:13Z","timestamp":1599571933000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}