{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T01:43:01Z","timestamp":1725500581979},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540775652"},{"type":"electronic","value":"9783540775669"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77566-9_28","type":"book-chapter","created":{"date-parts":[[2008,1,5]],"date-time":"2008-01-05T01:18:43Z","timestamp":1199495923000},"page":"328-339","source":"Crossref","is-referenced-by-count":4,"title":["Certification of Proving Termination of Term Rewriting by Matrix Interpretations"],"prefix":"10.1007","author":[{"given":"Adam","family":"Koprowski","sequence":"first","affiliation":[]},{"given":"Hans","family":"Zantema","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"The Coq proof assistant, http:\/\/coq.inria.fr"},{"key":"28_CR2","unstructured":"The RTA list of open problems, http:\/\/www.lsv.ens-cachan.fr\/rtaloop"},{"key":"28_CR3","unstructured":"Termination competition, http:\/\/www.lri.fr\/~marche\/termination-competition"},{"key":"28_CR4","unstructured":"Termination problems data base, http:\/\/www.lri.fr\/~marche\/tpdb"},{"issue":"1-2","key":"28_CR5","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science\u00a0236(1-2), 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"28_CR6","unstructured":"Blanqui, F., Delobel, W., Coupet-Grimal, S., Hinderer, S., Koprowski, A.: CoLoR, a Coq library on rewriting and termination. In: 8th WST (2006)"},{"key":"28_CR7","series-title":"LNCS(LNAI)","first-page":"148","volume-title":"FroCoS 2007","author":"\u00c9. Contejean","year":"2007","unstructured":"Contejean, \u00c9., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Certification of automated termination proofs. In: Konev, B., Wolter, F. (eds.) FroCoS 2007. LNCS(LNAI), vol.\u00a04720, pp. 148\u2013162. Springer, Heidelberg (to appear, 2007)"},{"key":"28_CR8","unstructured":"Contejean, E., March\u00e9, C., Monate, B., Urbain, X.: The CiME rewrite tool, http:\/\/cime.lri.fr"},{"key":"28_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/11814771_47","volume-title":"Automated Reasoning","author":"J. Endrullis","year":"2006","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 574\u2013588. Springer, Heidelberg (2006)"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning (accepted, 2007)","DOI":"10.1007\/11814771_47"},{"key":"28_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-3-540-32275-7_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"issue":"4","key":"28_CR12","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1016\/j.ic.2006.08.010","volume":"205","author":"N. Hirokawa","year":"2007","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. Information and Computation\u00a0205(4), 474\u2013511 (2007)","journal-title":"Information and Computation"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11805618_19","volume-title":"Term Rewriting and Applications","author":"A. Koprowski","year":"2006","unstructured":"Koprowski, A.: TPA: Termination proved automatically. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 257\u2013266. Springer, Heidelberg (2006)"},{"key":"28_CR14","unstructured":"Koprowski, A., Zantema, H.: Certification of matrix interpretations in Coq. In: 9th WST (2007)"},{"key":"28_CR15","unstructured":"Koprowski, A., Zantema, H.: Certification of proving termination of term rewriting by matrix interpretations. Technical Report CS-Report 07\/22, Eindhoven University of Technology (August 2007), http:\/\/www.win.tue.nl\/~akoprows\/papers\/mint-cert-TR.pdf"},{"key":"28_CR16","series-title":"LNAI","first-page":"460","volume-title":"CADE 2007","author":"A. Krauss","year":"2007","unstructured":"Krauss, A.: Certified size-change termination. In: CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 460\u2013475. Springer, Heidelberg (2007)"},{"key":"28_CR17","unstructured":"Magaud, N.: Ring properties for square matrices. Coq contributions, http:\/\/coq.inria.fr\/contribs-eng.html"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/978-3-540-73449-9_23","volume-title":"RTA 2007","author":"C. March\u00e9","year":"2007","unstructured":"March\u00e9, C., Zantema, H.: The Termination Competition 2007. In: RTA 2007. LNCS, vol.\u00a04533, pp. 303\u2013313. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2008: Theory and Practice of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77566-9_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:44:55Z","timestamp":1619505895000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77566-9_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540775652","9783540775669"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77566-9_28","relation":{},"subject":[]}}