{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T03:46:58Z","timestamp":1743047218843,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319669014"},{"type":"electronic","value":"9783319669021"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66902-1_18","type":"book-chapter","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T07:34:20Z","timestamp":1503992060000},"page":"295-310","source":"Crossref","is-referenced-by-count":1,"title":["Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent"],"prefix":"10.1007","author":[{"given":"Reuben N. S.","family":"Rowe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Brotherston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,30]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of Mathematical Logic","author":"P Aczel","year":"1977","unstructured":"Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 739\u2013782. North-Holland, Amsterdam (1977)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-642-24372-1_37","volume-title":"Automated Technology for Verification and Analysis","author":"S Almagor","year":"2011","unstructured":"Almagor, S., Boker, U., Kupferman, O.: What\u2019s decidable about weighted automata? In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 482\u2013491. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-24372-1_37"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/11817963_35","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2006","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386\u2013400. Springer, Heidelberg (2006). doi:\n10.1007\/11817963_35"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","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, vol. 3702, pp. 78\u201392. Springer, Heidelberg (2005). doi:\n10.1007\/11554554_8"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-74061-2_6","volume-title":"Static Analysis","author":"J Brotherston","year":"2007","unstructured":"Brotherston, J.: Formalised inductive reasoning in the logic of bunched implications. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 87\u2013103. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-74061-2_6"},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1145\/1328438.1328453","volume":"43","author":"J Brotherston","year":"2008","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. ACM SIGPLAN Not. 43, 101\u2013112 (2008). doi:\n10.1145\/1328438.1328453\n\n. POPL-35. ACM","journal-title":"ACM SIGPLAN Not."},{"issue":"6","key":"18_CR7","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1093\/logcom\/exq052","volume":"21","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6), 1177\u20131216 (2011). doi:\n10.1093\/logcom\/exq052","journal-title":"J. Log. Comput."},{"key":"18_CR8","series-title":"Monographs in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01492-5","volume-title":"Handbook of Weighted Automata","author":"M Droste","year":"2009","unstructured":"Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata. Monographs in Theoretical Computer Science. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-01492-5"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_30","volume-title":"Automated Deduction \u2013 CADE 26","author":"G Tellez","year":"2017","unstructured":"Tellez, G., Brotherston, J.: Automatically verifying temporal properties of pointer programs with cyclic proof. In: de Moura, L. (ed.) CADE 2017. LNCS, vol. 10395. Springer, Cham (2017). doi:\n10.1007\/978-3-319-63046-5_30"},{"doi-asserted-by":"publisher","unstructured":"Filiot, E., Gentilini, R., Raskin, J.-F.: Finite-valued weighted automata. In: FSTTCS-34. LIPICS, vol. 29, pp. 133\u2013145 (2014). doi:\n10.4230\/LIPIcs.FSTTCS.2014.133","key":"18_CR10","DOI":"10.4230\/LIPIcs.FSTTCS.2014.133"},{"doi-asserted-by":"publisher","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proceedings of the POPL-28, pp. 14\u201326. ACM (2001). doi:\n10.1145\/373243.375719","key":"18_CR11","DOI":"10.1145\/373243.375719"},{"issue":"1","key":"18_CR12","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1137\/0204007","volume":"4","author":"DB Johnson","year":"1975","unstructured":"Johnson, D.B.: Finding all the elementary circuits of a directed graph. SIAM J. Comput. 4(1), 77\u201384 (1975). doi:\n10.1137\/0204007","journal-title":"SIAM J. Comput."},{"issue":"3","key":"18_CR13","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1142\/S0218196794000063","volume":"4","author":"D Krob","year":"1994","unstructured":"Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. IJAC 4(3), 405\u2013426 (1994). doi:\n10.1142\/S0218196794000063","journal-title":"IJAC"},{"doi-asserted-by":"publisher","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL-28, pp. 81\u201392. ACM (2001). doi:\n10.1145\/373243.360210","key":"18_CR14","DOI":"10.1145\/373243.360210"},{"key":"18_CR15","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/S0049-237X(08)70847-4","volume-title":"2nd Scandinavian Logic Symposium","author":"P Martin-L\u00f6f","year":"1971","unstructured":"Martin-L\u00f6f, P.: Hauptsatz for the intuitionistic theory of iterated inductive definitions. 2nd Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 179\u2013216. North-Holland, Amsterdam (1971)"},{"doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the LICS-17, pp. 55\u201374. IEEE (2002). doi:\n10.1109\/LICS.2002.1029817","key":"18_CR16","DOI":"10.1109\/LICS.2002.1029817"},{"doi-asserted-by":"publisher","unstructured":"Rowe, R.N.S., Brotherston, J.: Automatic cyclic termination proofs for recursive procedures in separation logic. In: CPP-6, pp. 53\u201365. ACM (2017). doi:\n10.1145\/3018610.3018623","key":"18_CR17","DOI":"10.1145\/3018610.3018623"},{"unstructured":"Rowe, R.N.S., Brotherston, J.: Size relationships in abstract cyclic entailment systems. Technical report (2017). \nhttps:\/\/arxiv.org\/abs\/1702.03981","key":"18_CR18"},{"issue":"2","key":"18_CR19","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/0304-3975(91)90381-B","volume":"88","author":"A Weber","year":"1991","unstructured":"Weber, A., Seidl, H.: On the degree of ambiguity of finite automata. Theor. Comput. Sci. 88(2), 325\u2013349 (1991). doi:\n10.1016\/0304-3975(91)90381-B","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66902-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,11,14]],"date-time":"2017-11-14T05:58:10Z","timestamp":1510639090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66902-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319669014","9783319669021"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66902-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}