{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,15]],"date-time":"2024-07-15T00:09:15Z","timestamp":1721002155210},"reference-count":33,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2019,2,1]]},"DOI":"10.1587\/transinf.2017edp7368","type":"journal-article","created":{"date-parts":[[2019,1,31]],"date-time":"2019-01-31T22:45:02Z","timestamp":1548974702000},"page":"223-238","source":"Crossref","is-referenced-by-count":0,"title":["Multi-Context Automated Lemma Generation for Term Rewriting Induction with Divergence Detection"],"prefix":"10.1587","volume":"E102.D","author":[{"given":"Chengcheng","family":"JI","sequence":"first","affiliation":[{"name":"Graduate School of Information Science and Technology, Hokkaido University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masahito","family":"KURIHARA","sequence":"additional","affiliation":[{"name":"Graduate School of Information Science and Technology, Hokkaido University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haruhiko","family":"SATO","sequence":"additional","affiliation":[{"name":"Faculty of Engineering, Hokkai-Gakuen University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"[1] T. Aoto, \u201cDealing with non-orientable equations in rewriting induction,\u201d Proc. 17th International Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol.4098, pp.242-256, 2006. 10.1007\/11805618_18","DOI":"10.1007\/11805618_18"},{"key":"2","unstructured":"[2] T. Aoto, \u201cRewriting induction using termination checker,\u201d JSSST 24th Annual Conf., 3C-3, 2007 (in Japanese)."},{"key":"3","unstructured":"[3] T. Aoto, \u201cDesigning a rewriting induction prover with an increased capability of nonorientable equations,\u201d Proc. Symbolic Computation in Software Science AustrianJapanese Workshop, RISC Technical Report, vol.08-08, pp.1-15, 2008."},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] T. Arts and J. Giesl, \u201cTermination of term rewriting using dependency pairs,\u201d Theor. Comput. Sci., vol.236, no.1-2, pp.133-178, 2000. 10.1016\/s0304-3975(99)00207-8","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] F. Baader and T. Nipkow, Term Rewriting and All That, Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] D. Basin and T. Walsh, \u201cDifference matching,\u201d Proc. 11th International Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol.607, pp.295-309, 1992. 10.1007\/3-540-55602-8_173","DOI":"10.1007\/3-540-55602-8_173"},{"key":"7","unstructured":"[7] D. Basin and T. Walsh, \u201cDifference unification,\u201d Proc. 13th International Joint Conf. of Artificial Intelligence, pp.116-122, 1993."},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] D.A. Basin and T. Walsh, \u201cTermination orderings for rippling,\u201d Proc. 12th International Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol.814, pp.466-483, 1994. 10.1007\/3-540-58156-1_34","DOI":"10.1007\/3-540-58156-1_34"},{"key":"9","unstructured":"[9] R.S. Boyer and J.S. Moore, A Computational Logic, Academic Press, New York, 1979."},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill, \u201cRippling: A heuristic for guiding inductive proofs,\u201d Artificial Intelligence, vol.62, no.2, pp.185-253, 1993. 10.1016\/0004-3702(93)90079-q","DOI":"10.1016\/0004-3702(93)90079-Q"},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] N. Dershowitz and J.-P. Jouannaud, \u201cRewrite systems,\u201d in Handbook of Theoretical Computer Science, ed. J. van Leeuwen, vol.B, pp.243-320, MIT Press, 1990. 10.1016\/b978-0-444-88074-1.50011-1","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"12","doi-asserted-by":"crossref","unstructured":"[12] C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl, \u201cSAT solving for termination analysis with polynomial interpretations,\u201d Proc. 10th International Conf. on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, vol.4501, pp.340-354, 2007. 10.1007\/978-3-540-72788-0_33","DOI":"10.1007\/978-3-540-72788-0_33"},{"key":"13","doi-asserted-by":"publisher","unstructured":"[13] J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke, \u201cMechanizing and improving dependency pairs,\u201d J. Autom. Reasoning., vol.37, no.3, pp.155-203, 2006. 10.1007\/s10817-006-9057-7","DOI":"10.1007\/s10817-006-9057-7"},{"key":"14","doi-asserted-by":"publisher","unstructured":"[14] N. Hirokawa and A. Middeldorp, \u201cTyrolean termination tool: Techniques and features,\u201d Inform. Comput., vol.205, no.4, pp.474-511, 2007. 10.1016\/j.ic.2006.08.010","DOI":"10.1016\/j.ic.2006.08.010"},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] G. Huet and J.-M. Hullot, \u201cProofs by induction in equational theories with constructors,\u201d J. Comput. Syst. Sci., vol.25, pp.239-266, 1982. 10.1016\/0022-0000(82)90006-x","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"16","doi-asserted-by":"crossref","unstructured":"[16] D. Hutter, \u201cGuiding induction proofs,\u201d Proc. 10th International Conf. on Automated Deduction, Lecture Notes in Artificial Intelligence, vol.449, pp.147-161, 1990. 10.1007\/3-540-52885-7_85","DOI":"10.1007\/3-540-52885-7_85"},{"key":"17","unstructured":"[17] CC. Ji, H. Sato, and M. Kurihara, \u201cA new implementation of multi-context algebraic inductive theorem prover,\u201d Lecture Notes in Engineering and Computer Science: Proc. The World Congress on Engineering and Computer Science 2015, pp.109-114, 2015."},{"key":"18","doi-asserted-by":"publisher","unstructured":"[18] M. Johansson, L. Dixon, and A. Bundy, \u201cConjecture synthesis for inductive theories,\u201d J. Autom. Reasoning., vol.47, no.3, pp.251-289, 2011. 10.1007\/s10817-010-9193-y","DOI":"10.1007\/s10817-010-9193-y"},{"key":"19","doi-asserted-by":"crossref","unstructured":"[19] J.W. Klop, \u201cTerm rewriting systems,\u201d in Handbook of Logic in Computer Science, ed. S. Abramsky et al., pp.1-116, Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0001"},{"key":"20","doi-asserted-by":"publisher","unstructured":"[20] M. Kurihara and H. Kondo, \u201cCompletion for multiple reduction orderings,\u201d J. Autom. Reasoning., vol.23, no.1, pp.25-42, 1999. 10.1023\/a:1006129631807","DOI":"10.1023\/A:1006129631807"},{"key":"21","doi-asserted-by":"crossref","unstructured":"[21] D.R. Musser, \u201cOn proving induction properties of abstract data types,\u201d Proc. 7th ACM Symposium on Principles of Programming Languages, pp.154-162, 1980. 10.1145\/567446.567461","DOI":"10.1145\/567446.567461"},{"key":"22","doi-asserted-by":"publisher","unstructured":"[22] P. Urso and E. Kounalis, \u201cSound generalizations in mathematical induction,\u201d Theor. Comput. Sci., vol.323, pp.443-471, 2004. 10.1016\/j.tcs.2004.05.022","DOI":"10.1016\/j.tcs.2004.05.022"},{"key":"23","doi-asserted-by":"publisher","unstructured":"[23] D.A. Plaisted, \u201cSemantic confluence tests and completion methods,\u201d Inform. Comput., vol.65, no.2-3, pp.182-215, 1985. 10.1016\/s0019-9958(85)80005-x","DOI":"10.1016\/S0019-9958(85)80005-X"},{"key":"24","doi-asserted-by":"crossref","unstructured":"[24] D.A. Plaisted, \u201cEquational reasoning and term rewriting systems,\u201d in Handbook of Logic in Artificial Intelligence and Logic Programming, ed. D.M. Gabbay et al., vol.1, pp.274-367, Oxford Univ. Press, 1993.","DOI":"10.1093\/oso\/9780198537458.003.0005"},{"key":"25","doi-asserted-by":"crossref","unstructured":"[25] U.S. Reddy, \u201cTerm rewriting induction,\u201d Proc. 10th International Conf. on Automated Deduction, Lecture Notes in Computer Science, vol.449, pp.162-177, 1990. 10.1007\/3-540-52885-7_86","DOI":"10.1007\/3-540-52885-7_86"},{"key":"26","doi-asserted-by":"publisher","unstructured":"[26] H. Sato and M. Kurihara, \u201cMulti-context rewriting induction with termination checkers,\u201d IEICE Trans. Inf. & Syst., vol.E93-D, no.5, pp.942-952, 2010. 10.1587\/transinf.e93.d.942","DOI":"10.1587\/transinf.E93.D.942"},{"key":"27","doi-asserted-by":"crossref","unstructured":"[27] H. Sato, S. Winkler, M. Kurihara, and A. Middeldorp, \u201cMulti-completion with termination tools (system description),\u201d Proc. 4th International Joint Conf. on Automated Reasoning, Lecture Notes in Artificial Intelligence, vol.5195, pp.306-312, 2008. 10.1007\/978-3-540-71070-7_26","DOI":"10.1007\/978-3-540-71070-7_26"},{"key":"28","doi-asserted-by":"publisher","unstructured":"[28] H. Sato, M. Kurihara, S. Winkler, and A. Middeldorp, \u201cConstraint-based multi-completion procedures for term rewriting systems,\u201d IEICE Trans. Inf. & Syst., vol.E92-D, no.2, pp.220-234, 2009. 10.1587\/transinf.e92.d.220","DOI":"10.1587\/transinf.E92.D.220"},{"key":"29","unstructured":"[29] S. Shimazu, T. Aoto, and Y. Toyama. \u201cAutomated lemma generation for rewriting induction with disproof,\u201d Computer Software, vol.26, no.2, pp.41-55, 2009 (in Japanese)."},{"key":"30","unstructured":"[30] Terese, Term Rewriting Systems, Cambridge University Press, 2003."},{"key":"31","doi-asserted-by":"publisher","unstructured":"[31] T. Walsh, \u201cA divergence critic for inductive proof,\u201d J. Artif. Intell. Res., vol.4, pp.209-235, 1996. 10.1613\/jair.275","DOI":"10.1613\/jair.275"},{"key":"32","doi-asserted-by":"crossref","unstructured":"[32] I. Wehrman, A. Stump, and E. Westbrook, \u201cSlothrop: Knuth-Bendix completion with a modern termination checker,\u201d Proc. 17th International Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol.4098, pp.287-296, 2006. 10.1007\/11805618_22","DOI":"10.1007\/11805618_22"},{"key":"33","doi-asserted-by":"crossref","unstructured":"[33] C.-P. Wirth, \u201cHistory and future of implicit and inductionless induction: beware the old jade and the zombie!,\u201d in Mechanizing Mathematical Reasoning, Lecture Notes in Artificial Intelligence, vol.2605, pp.192-203, 2005. 10.1007\/978-3-540-32254-2_12","DOI":"10.1007\/978-3-540-32254-2_12"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E102.D\/2\/E102.D_2017EDP7368\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,14]],"date-time":"2024-07-14T13:19:17Z","timestamp":1720963157000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E102.D\/2\/E102.D_2017EDP7368\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,1]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2017edp7368","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,2,1]]}}}