{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:33:15Z","timestamp":1743103995861,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030994600"},{"type":"electronic","value":"9783030994617"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-99461-7_15","type":"book-chapter","created":{"date-parts":[[2022,5,2]],"date-time":"2022-05-02T23:02:40Z","timestamp":1651532560000},"page":"262-281","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On Transforming Cut- and Quantifier-Free Cyclic Proofs into\u00a0Rewriting-Induction Proofs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2377-1679","authenticated-orcid":false,"given":"Shujun","family":"Zhang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8697-4970","authenticated-orcid":false,"given":"Naoki","family":"Nishida","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,3]]},"reference":[{"key":"15_CR1","unstructured":"Aoto, T.: Rewriting induction using termination checkers. In: Proceedings of the JSSST 24th Annual Conference, pp. 1\u20134. No. 3C-C (2007). http:\/\/www.nue.ie.niigata-u.ac.jp\/~aoto\/research\/papers\/report\/itp.pdf. (in Japanese)"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Aoto, T., Toyama, Y.: Ground confluence prover based on rewriting induction. In: Kesner, D., Pientka, B. (eds.) Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction. LIPIcs, vol. 52, pp. 33:1\u201333:12. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.33","DOI":"10.4230\/LIPIcs.FSCD.2016.33"},{"key":"15_CR3","doi-asserted-by":"publisher","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752","DOI":"10.1017\/CBO9781139172752"},{"issue":"1","key":"15_CR4","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A Bouhoula","year":"1997","unstructured":"Bouhoula, A.: Automated theorem proving by test set induction. J. Symb. Comput. 23(1), 47\u201377 (1997). https:\/\/doi.org\/10.1006\/jsco.1996.0076","journal-title":"J. Symb. Comput."},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.jal.2011.09.001","volume":"10","author":"A Bouhoula","year":"2012","unstructured":"Bouhoula, A., Jacquemard, F.: Sufficient completeness verification for conditional and constrained TRS. J. Appl. Log. 10(1), 127\u2013143 (2012). https:\/\/doi.org\/10.1016\/j.jal.2011.09.001","journal-title":"J. Appl. Log."},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/11554554_8","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J Brotherston","year":"2005","unstructured":"Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78\u201392. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11554554_8"},{"issue":"3","key":"15_CR7","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/s00165-016-0403-1","volume":"29","author":"P Fu","year":"2016","unstructured":"Fu, P., Komendantskaya, E.: Operational semantics of resolution and productivity in Horn clause logic. Formal Aspects Comput. 29(3), 453\u2013474 (2016). https:\/\/doi.org\/10.1007\/s00165-016-0403-1","journal-title":"Formal Aspects Comput."},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Fuhs, C., Kop, C., Nishida, N.: Verifying procedural programs via constrained rewriting induction. ACM Trans. Comput. Logic 18(2), 14:1\u201314:50 (2017). https:\/\/doi.org\/10.1145\/3060143","DOI":"10.1145\/3060143"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Kimura, D., Nakazawa, K., Terauchi, T., Unno, H.: Failure of cut-elimination in cyclic proofs of separation logic. Comput. Softw. 37(1), 39\u201352 (2020). https:\/\/doi.org\/10.11309\/jssst.37.1_39","DOI":"10.11309\/jssst.37.1_39"},{"issue":"6","key":"15_CR10","doi-asserted-by":"publisher","first-page":"990","DOI":"10.1017\/S1471068420000423","volume":"20","author":"E Komendantskaya","year":"2020","unstructured":"Komendantskaya, E., Rozplokhas, D., Basold, H.: The new normal: We cannot eliminate cuts in coinductive calculi, but we can explore them. Theory Pract. Logic Program. 20(6), 990\u20131005 (2020). https:\/\/doi.org\/10.1017\/S1471068420000423","journal-title":"Theory Pract. Logic Program."},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-40885-4_24","volume-title":"Frontiers of Combining Systems","author":"C Kop","year":"2013","unstructured":"Kop, C., Nishida, N.: Term rewriting with logical constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 343\u2013358. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_24"},{"issue":"1","key":"15_CR12","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0890-5401(90)90033-E","volume":"84","author":"A Lazrek","year":"1990","unstructured":"Lazrek, A., Lescanne, P., Thiel, J.: Tools for proving inductive equalities, relative completeness, and omega-completeness. Inf. Comput. 84(1), 47\u201370 (1990). https:\/\/doi.org\/10.1016\/0890-5401(90)90033-E","journal-title":"Inf. Comput."},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Mizutani, S., Nishida, N.: Transforming proof tableaux of Hoare logic into inference sequences of rewriting induction. In: Cirstea, H., Sabel, D. (eds.) Proceedings of the 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Electronic Proceedings in Theoretical Computer Science, vol. 265, pp. 35\u201351. Open Publishing Association (2018). https:\/\/doi.org\/10.4204\/EPTCS.265.4","DOI":"10.4204\/EPTCS.265.4"},{"key":"15_CR14","unstructured":"Nishie, K., Nishida, N., Sakai, M.: Extending rewriting induction to existentially quantified equations. IEICE Tech. Rep. SS2019-17 Inst. Electron. Inf. Commun. Eng. 119(246), 25\u201330 (2019). (in Japanese)"},{"key":"15_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3661-8","volume-title":"Advanced Topics in Term Rewriting","author":"E Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002). https:\/\/doi.org\/10.1007\/978-1-4757-3661-8"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-52885-7_86","volume-title":"10th International Conference on Automated Deduction","author":"US Reddy","year":"1990","unstructured":"Reddy, U.S.: Term rewriting induction. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 162\u2013177. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_86"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Rosu, G., Stefanescu, A., Ciob\u00e2c\u0103, \u015e., Moore, B.M.: One-path reachability logic. In: Proceedings of the 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 358\u2013367. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/LICS.2013.42","DOI":"10.1109\/LICS.2013.42"},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"Sato, H., Kurihara, M.: Multi-context rewriting induction with termination checkers. IEICE Trans. Inf. Syst. 93-D(5), 942\u2013952 (2010). https:\/\/doi.org\/10.1587\/transinf.E93.D.942","DOI":"10.1587\/transinf.E93.D.942"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Stratulat, S.: A unified view of induction reasoning for first-order logic. In: Turing-100. The Alan Turing Centenary. EPiC Series in Computing, vol. 10, pp. 326\u2013352. EasyChair (2012)","DOI":"10.29007\/nsx4"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Stratulat, S.: Structural vs. cyclic induction: a report on some experiments with Coq. In: Davenport, J.H., et al. (eds.) Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 29\u201336. IEEE (2016). https:\/\/doi.org\/10.1109\/SYNASC.2016.018","DOI":"10.1109\/SYNASC.2016.018"},{"key":"15_CR22","unstructured":"Terese: Term Rewriting Systems. No. 55 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498725","volume":"6","author":"T Tsukada","year":"2022","unstructured":"Tsukada, T., Unno, H.: Software model-checking as cyclic-proof search. Proc. ACM Program. Lang. 6, 1\u201329 (2022). https:\/\/doi.org\/10.1145\/3498725","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/978-3-319-63390-9_30","volume-title":"Computer Aided Verification","author":"H Unno","year":"2017","unstructured":"Unno, H., Torii, S., Sakamoto, H.: Automating induction for solving horn clauses. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 571\u2013591. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_30"},{"key":"15_CR25","doi-asserted-by":"publisher","unstructured":"Yamada, A., Sternagel, C., Thiemann, R., Kusakari, K.: AC dependency pairs revisited. In: Talbot, J., Regnier, L. (eds.) Proceedings of the 25th EACSL Annual Conference on Computer Science Logic. LIPIcs, vol. 62, pp. 8:1\u20138:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.8","DOI":"10.4230\/LIPIcs.CSL.2016.8"},{"key":"15_CR26","unstructured":"Zhang, S., Nishida, N.: On transforming inductive definition sets into term rewrite systems. In: Nakano, K., Riesco, A. (eds.) Informal Proceedings of the 8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, pp. 1\u201310 (2021). https:\/\/www.ipl.riec.tohoku.ac.jp\/wpte2021\/Zhang21wpte.pdf"},{"key":"15_CR27","unstructured":"Zhang, S., Nishida, N.: Transforming orthogonal inductive definition sets into confluent term rewrite systems, November 2021, https:\/\/www.trs.css.i.nagoya-u.ac.jp\/~nishida\/DB\/pdf\/ZhangNishida_21_wpte21-journal-submission.pdf. An extended version of [26] under submission to a journal"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99461-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,23]],"date-time":"2024-09-23T16:09:41Z","timestamp":1727107781000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99461-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030994600","9783030994617"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99461-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"3 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FLOPS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Functional and Logic Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"flops2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/flops-2022","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}