{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:04:40Z","timestamp":1750089880256,"version":"3.37.3"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,6,7]],"date-time":"2016-06-07T00:00:00Z","timestamp":1465257600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100003593","name":"CNPq","doi-asserted-by":"crossref","award":["UNIVERSAL 476952\/2013-1"],"award-info":[{"award-number":["UNIVERSAL 476952\/2013-1"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100005668","name":"FAPDF","doi-asserted-by":"crossref","award":["PRONEX 2009\/00091-0"],"award-info":[{"award-number":["PRONEX 2009\/00091-0"]}],"id":[{"id":"10.13039\/501100005668","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,2]]},"DOI":"10.1007\/s10817-016-9376-2","type":"journal-article","created":{"date-parts":[[2016,6,7]],"date-time":"2016-06-07T06:07:15Z","timestamp":1465279635000},"page":"231-251","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System"],"prefix":"10.1007","volume":"58","author":[{"given":"Ana Cristina","family":"Rocha-Oliveira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9 Luiz","family":"Galdino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,7]]},"reference":[{"issue":"5","key":"9376_CR1","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1093\/jigpal\/jzu012","volume":"22","author":"A Avelar","year":"2014","unstructured":"Avelar, A., Galdino, A., de Moura, F., Ayala-Rinc\u00f3n, M.: First-order unification in the PVS proof assistant. Logic J. IGPL 22(5), 758\u2013789 (2014)","journal-title":"Logic J. IGPL"},{"key":"9376_CR2","unstructured":"Ayala-Rinc\u00f3n, M., Avelar, A.B., Galdino, A.L., Rocha-Oliveira, A.C.: TRS: a PVS Theory for Term Rewriting Systems. http:\/\/trs.cic.unb.br \u2014Universidade de Bras\u00edlia, and http:\/\/shemesh.larc.nasa.gov\/fm\/ftp\/larc\/PVS-library\/library.html \u2014NASA Langley Research Center PVS libraries (Last visited: August, 2015)"},{"key":"9376_CR3","doi-asserted-by":"crossref","unstructured":"Ayala-Rinc\u00f3n, M., Fern\u00e1ndez, M., Gabbay, M.J., Rocha-Oliveira, A.C.: Checking overlaps of nominal rewriting rules. In Pre-proc. Logical and Semantic Frameworks with Applications (LSFA). ENTCS (2015)","DOI":"10.1016\/j.entcs.2016.06.004"},{"key":"9376_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"volume-title":"Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science","year":"2003","key":"9376_CR5","unstructured":"Bezem, M., Klop, J.W., de Vrijer, R. (eds.): Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)"},{"issue":"1","key":"9376_CR6","first-page":"39","volume":"1","author":"AL Galdino","year":"2008","unstructured":"Galdino, A.L., Ayala-Rinc\u00f3n, M.: A formalization of Newman\u2019s and Yokouchi\u2019s lemmas in a higher-order language. J. Formal. Reason. 1(1), 39\u201350 (2008)","journal-title":"J. Formal. Reason."},{"issue":"3","key":"9376_CR7","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/s10817-010-9165-2","volume":"45","author":"AL Galdino","year":"2010","unstructured":"Galdino, A.L., Ayala-Rinc\u00f3n, M.: A formalization of the Knuth\u2013Bendix(\u2013Huet) critical pair theorem. J. Autom. Reason. 45(3), 301\u2013325 (2010)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9376_CR8","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"GP Huet","year":"1980","unstructured":"Huet, G.P.: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797\u2013821 (1980)","journal-title":"J. ACM"},{"key":"9376_CR9","unstructured":"Huet, G.P., L\u00e9vy, J.-J.: Computations in orthogonal rewriting systems, I. In: Computational Logic\u2014Essays in Honor of Alan Robinson, pp. 395\u2013414 (1991)"},{"key":"9376_CR10","doi-asserted-by":"crossref","unstructured":"Rocha-Oliveira, A.C., Ayala-Rinc\u00f3n, M.: Formalizing the confluence of orthogonal rewriting systems. In: Proceedings of 7th Workshop on Logical and Semantic Frameworks, with Applications, LSFA, pp. 145\u2013152 (2012)","DOI":"10.4204\/EPTCS.113.14"},{"issue":"1","key":"9376_CR11","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"BK Rosen","year":"1973","unstructured":"Rosen, B.K.: Tree-manipulating systems and Church\u2013Rosser theorems. J. ACM 20(1), 160\u2013187 (1973)","journal-title":"J. ACM"},{"key":"9376_CR12","unstructured":"Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Prover Guide. Technical report, SRI International. http:\/\/pvs.csl.sri.com\/doc\/pvs-prover-guide.pdf (2001)"},{"key":"9376_CR13","unstructured":"Suzuki, T., Kikuchi, K., Aoto, T., Toyama, Y.: Confluence of orthogonal nominal rewriting systems revisited. In: Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), pp. 301\u2013317. LIPIcs (2015)"},{"issue":"1","key":"9376_CR14","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M Takahashi","year":"1995","unstructured":"Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120\u2013127 (1995)","journal-title":"Inf. Comput."},{"key":"9376_CR15","doi-asserted-by":"crossref","unstructured":"Thiemann, R.: Formalizing bounded increase. In: Interactive Theorem Proving\u20144th International Conference, ITP 2013, Rennes, France, July 22\u201326, 2013. Proceedings, pp. 245\u2013260 (2013)","DOI":"10.1007\/978-3-642-39634-2_19"},{"issue":"1","key":"9376_CR16","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/S0304-3975(96)00173-9","volume":"175","author":"V Oostrom van","year":"1997","unstructured":"van Oostrom, V.: Developing developments. Theor. Comput. Sci. 175(1), 159\u2013181 (1997)","journal-title":"Theor. Comput. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9376-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9376-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9376-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9376-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T05:57:39Z","timestamp":1568008659000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9376-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,7]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,2]]}},"alternative-id":["9376"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9376-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2016,6,7]]}}}