{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:17:05Z","timestamp":1762460225472,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,9,5]],"date-time":"2016-09-05T00:00:00Z","timestamp":1473033600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,9,5]]},"DOI":"10.1145\/2967973.2968598","type":"proceedings-article","created":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T18:25:14Z","timestamp":1472754314000},"page":"50-61","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Proving inductive validity of constrained inequalities"],"prefix":"10.1145","author":[{"given":"Takahiro","family":"Nagao","sequence":"first","affiliation":[{"name":"Nagoya University, Nagoya, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Nishida","sequence":"additional","affiliation":[{"name":"Nagoya University, Nagoya, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,9,5]]},"reference":[{"unstructured":"T. Aoto. Soundness of rewriting induction based on an abstract principle. IPSJ Transactions on Programming 49(SIG 1 (PRO 35)):28--38 2008.  T. Aoto. Soundness of rewriting induction based on an abstract principle. IPSJ Transactions on Programming 49(SIG 1 (PRO 35)):28--38 2008.","key":"e_1_3_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1016\/S0304-3975(99)00207-8"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.5555\/280474"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.1006\/jsco.1996.0076"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.1007\/978-3-540-71070-7_44"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1016\/j.jal.2011.09.001"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1007\/BF00881856"},{"volume-title":"Academic Press","year":"1979","author":"Boyer R. S.","key":"e_1_3_2_1_8_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"doi-asserted-by":"crossref","unstructured":"A.\n       \n      Bundy F.\n       \n      van Harmelen A.\n       \n      Smaill and \n      \n      \n      A.\n       \n      Ireland\n      \n  \n  . \n  Extensions to the rippling-out tactic for guiding inductive proofs. In M. E. Stickel editor Proceedings of the 10th International Conference on Automated Deduction volume \n  449\n   of \n  Lecture Notes in Artificial Intelligence pages \n  132\n  --\n  146\n  . \n  Springer 1990\n  .   A. Bundy F. van Harmelen A. Smaill and A. Ireland. Extensions to the rippling-out tactic for guiding inductive proofs. In M. E. Stickel editor Proceedings of the 10th International Conference on Automated Deduction volume 449 of Lecture Notes in Artificial Intelligence pages 132--146. Springer 1990.","key":"e_1_3_2_1_10_1","DOI":"10.1007\/3-540-52885-7_84"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1007\/978-3-540-70590-1_7"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1007\/978-3-642-31365-3_20"},{"issue":"2","key":"e_1_3_2_1_13_1","first-page":"100","article-title":"Approach to procedural-program verification based on implicit induction of constrained term rewriting systems","volume":"1","author":"Furuichi Y.","year":"2008","journal-title":"IPSJ Transactions on Programming"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1016\/0022-0000(82)90006-X"},{"volume-title":"Cambridge University Press","year":"2000","author":"Huth M.","key":"e_1_3_2_1_15_1"},{"issue":"6","key":"e_1_3_2_1_16_1","first-page":"1","article-title":"Inductionless induction and rewriting induction","volume":"17","author":"Koike H.","year":"2000","journal-title":"Computer Software"},{"key":"e_1_3_2_1_17_1","first-page":"59","volume-title":"Proceedings of the 13th International Workshop on Termination","author":"Kop C.","year":"2013"},{"doi-asserted-by":"crossref","unstructured":"C.\n       \n      Kop\n     and \n      \n      \n      N.\n       \n      Nishida\n      \n  \n  . \n  Term rewriting with logical constraints. In P. Fontaine C. Ringeissen and R. A. Schmidt editors Proceedings of the 9th International Symposium on Frontiers of Combining Systems volume \n  8152\n   of \n  Lecture Notes in Artificial Intelligence pages \n  343\n  --\n  358\n  . \n  Springer 2013\n  .  C. Kop and N. Nishida. Term rewriting with logical constraints. In P. Fontaine C. Ringeissen and R. A. Schmidt editors Proceedings of the 9th International Symposium on Frontiers of Combining Systems volume 8152 of Lecture Notes in Artificial Intelligence pages 343--358. Springer 2013.","key":"e_1_3_2_1_18_1","DOI":"10.1007\/978-3-642-40885-4_24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_19_1","DOI":"10.1007\/978-3-319-12736-1_18"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1145\/567446.567461"},{"issue":"1","key":"e_1_3_2_1_21_1","first-page":"173","article-title":"Lemma generation method in rewriting induction for constrained term rewriting systems","volume":"28","author":"Nakabayashi N.","year":"2010","journal-title":"Computer Software"},{"key":"e_1_3_2_1_22_1","first-page":"24","volume-title":"Proceedings of the 1st International Workshop on Trends in Tree Automata and Tree Transducers","author":"Nishida N.","year":"2012"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.4204\/EPTCS.134.1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.5555\/648229.752322"},{"doi-asserted-by":"crossref","unstructured":"T.\n       \n      Sakata N.\n       \n      Nishida and \n      \n      \n      T.\n       \n      Sakabe\n      \n  \n  . \n  On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs. In H. Kuchen editor Proceedings of the 20th International Workshop on Functional and Constraint Logic Programming volume \n  6816\n   of \n  Lecture Notes in Computer Science pages \n  138\n  --\n  155\n  . \n  Springer 2011\n  .   T. Sakata N. Nishida and T. Sakabe. On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs. In H. Kuchen editor Proceedings of the 20th International Workshop on Functional and Constraint Logic Programming volume 6816 of Lecture Notes in Computer Science pages 138--155. Springer 2011.","key":"e_1_3_2_1_25_1","DOI":"10.1007\/978-3-642-22531-4_9"},{"issue":"2","key":"e_1_3_2_1_26_1","first-page":"80","article-title":"Rewriting induction for constrained term rewriting systems","volume":"2","author":"Sakata T.","year":"2009","journal-title":"IPSJ Transactions on Programming"}],"event":{"sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"acronym":"PPDP '16","name":"PPDP '16: 18th International Symposium on Principles and Practice of Declarative Programming","location":"Edinburgh United Kingdom"},"container-title":["Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2967973.2968598","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2967973.2968598","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:07:03Z","timestamp":1750223223000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2967973.2968598"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,5]]},"references-count":26,"alternative-id":["10.1145\/2967973.2968598","10.1145\/2967973"],"URL":"https:\/\/doi.org\/10.1145\/2967973.2968598","relation":{},"subject":[],"published":{"date-parts":[[2016,9,5]]},"assertion":[{"value":"2016-09-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}