{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:32:36Z","timestamp":1742916756312,"version":"3.40.3"},"publisher-location":"Cham","reference-count":8,"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":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Proof terms are a useful concept for comparing computations in term rewriting. We analyze proof terms with composition, with an eye towards automation. We revisit permutation equivalence and projection equivalence, two key notions presented in the literature. We report on the integration of proof terms with composition into ProTeM, a tool for manipulating proof terms.<\/jats:p>","DOI":"10.1007\/978-3-030-29436-6_20","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"337-353","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Composing Proof Terms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8470-2485","authenticated-orcid":false,"given":"Christina","family":"Kohl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7366-8464","authenticated-orcid":false,"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752","journal-title":"Cambridge University Press"},{"issue":"4","key":"20_CR2","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s10817-011-9238-x","volume":"47","author":"N Hirokawa","year":"2011","unstructured":"Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. J. Autom. Reasoning 47(4), 481\u2013501 (2011). https:\/\/doi.org\/10.1007\/s10817-011-9238-x","journal-title":"J. Autom. Reasoning"},{"key":"20_CR3","doi-asserted-by":"publisher","unstructured":"Kohl, C., Middeldorp, A.: ProTeM: a proof term manipulator (system description). In: Kirchner, H. (ed.) Proceedings of 3rd International Conference on Formal Structures for Computation and Deduction. Leibniz International Proceedings in Informatics, vol. 108, pp. 31:1\u201331:8 (2018). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.31","DOI":"10.4230\/LIPIcs.FSCD.2018.31"},{"issue":"2","key":"20_CR4","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0304-3975(01)00357-7","volume":"285","author":"N Mart\u00ed-Oliet","year":"2002","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theoret. Comput. Sci. 285(2), 121\u2013154 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00357-7","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"20_CR5","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","journal-title":"Theoret. Comput. Sci."},{"key":"20_CR6","doi-asserted-by":"publisher","unstructured":"van Oostrom, V., de Vrijer, R.: Four equivalent equivalences of reductions. In: Proceedings of 2nd International Workshop on Reduction Strategies in Rewriting and Programming. Electronic Notes in Theoretical Computer Science, vol. 70(6), pp. 21\u201361 (2002). https:\/\/doi.org\/10.1016\/S1571-0661(04)80599-1","DOI":"10.1016\/S1571-0661(04)80599-1"},{"key":"20_CR7","unstructured":"Terese (ed.): Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)"},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"89","DOI":"10.3233\/FI-1995-24124","volume":"24","author":"H Zantema","year":"1995","unstructured":"Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89\u2013105 (1995). https:\/\/doi.org\/10.3233\/FI-1995-24124","journal-title":"Fundamenta Informaticae"}],"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_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:56:40Z","timestamp":1657576600000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_20","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"}}]}}