{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T15:43:18Z","timestamp":1774626198813,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642351815","type":"print"},{"value":"9783642351822","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35182-2_25","type":"book-chapter","created":{"date-parts":[[2012,12,6]],"date-time":"2012-12-06T01:19:15Z","timestamp":1354756755000},"page":"350-367","source":"Crossref","is-referenced-by-count":66,"title":["A Generic Cyclic Theorem Prover"],"prefix":"10.1007","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[]},{"given":"Nikos","family":"Gorogiannis","sequence":"additional","affiliation":[]},{"given":"Rasmus L.","family":"Petersen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"Cyclist framework download, http:\/\/www.cs.ucl.ac.uk\/staff\/ngorogia\/"},{"key":"25_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-45085-6_29","volume-title":"Automated Deduction \u2013 CADE-19","author":"J. Avenhaus","year":"2003","unstructured":"Avenhaus, J., K\u00fchler, U., Schmidt-Samoa, T., Wirth, C.-P.: How to Prove Inductive Theorems? QuodLibet! In: Baader, F. (ed.) CADE-19. LNCS (LNAI), vol.\u00a02741, pp. 328\u2013333. Springer, Heidelberg (2003)"},{"key":"25_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.\u00a04144, pp. 386\u2013400. Springer, Heidelberg (2006)"},{"key":"25_CR4","series-title":"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.\u00a03702, pp. 78\u201392. Springer, Heidelberg (2005)"},{"key":"25_CR5","unstructured":"Brotherston, J.: Sequent Calculus Proof Systems for Inductive Definitions. Ph.D. thesis, University of Edinburgh (November 2006)"},{"key":"25_CR6","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: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 87\u2013103. Springer, Heidelberg (2007)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: POPL-35, pp. 101\u2013112. ACM (2008)","DOI":"10.1145\/1328438.1328453"},{"key":"25_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-22438-6_12","volume-title":"Automated Deduction \u2013 CADE-23","author":"J. Brotherston","year":"2011","unstructured":"Brotherston, J., Distefano, D., Petersen, R.L.: Automated Cyclic Entailment Proofs in Separation Logic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 131\u2013146. Springer, Heidelberg (2011)"},{"issue":"6","key":"25_CR9","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. Journal of Logic and Computation\u00a021(6), 1177\u20131216 (2011)","journal-title":"Journal of Logic and Computation"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Handbook of Automated Reasoning, vol.\u00a0I, ch. 13, pp. 845\u2013911. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM\u201999 - Formal Methods","author":"J.-M. Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly Verification of Linear Temporal Logic. In: Wing, J., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 253\u2013271. Springer, Heidelberg (1999)"},{"key":"25_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction \u2013 CADE-19","author":"L. Dixon","year":"2003","unstructured":"Dixon, L., Fleuriot, J.: IsaPlanner: A Prototype Proof Planner in Isabelle. In: Baader, F. (ed.) CADE-19. LNCS (LNAI), vol.\u00a02741, pp. 279\u2013283. Springer, Heidelberg (2003)"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D.: Spot: An extensible model checking library using transition-based generalized B\u00fcchi automata. In: MASCOTS, pp. 76\u201383 (2004)","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-00768-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Fogarty","year":"2009","unstructured":"Fogarty, S., Vardi, M.Y.: B\u00fcchi Complementation and Size-Change Termination. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 16\u201330. Springer, Heidelberg (2009)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-30476-0_10","volume-title":"Automated Technology for Verification and Analysis","author":"E. Friedgut","year":"2004","unstructured":"Friedgut, E., Kupferman, O., Vardi, M.Y.: B\u00fcchi Complementation Made Tighter. In: Wang, F. (ed.) ATVA 2004. LNCS, vol.\u00a03299, pp. 64\u201378. Springer, Heidelberg (2004)"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. Journal of Automated Reasoning 47(3) (October 2011)","DOI":"10.1007\/s10817-010-9193-y"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"25_CR18","doi-asserted-by":"crossref","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":"10.1145\/373243.360210"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-70545-1_34","volume-title":"Computer Aided Verification","author":"H.H. Nguyen","year":"2008","unstructured":"Nguyen, H.H., Chin, W.N.: Enhancing Program Verification with Lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 355\u2013369. Springer, Heidelberg (2008)"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/3-540-45931-6_26","volume-title":"Foundations of Software Science and Computation Structures","author":"U. Sch\u00f6pp","year":"2002","unstructured":"Sch\u00f6pp, U., Simpson, A.: Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 372\u2013386. Springer, Heidelberg (2002)"},{"key":"25_CR21","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1051\/ita:2003024","volume":"37","author":"C. Sprenger","year":"2003","unstructured":"Sprenger, C., Dam, M.: A note on global induction mechanisms in a \u03bc-calculus with explicit approximations. Theor. Informatics and Applications\u00a037, 365\u2013399 (2003)","journal-title":"Theor. Informatics and Applications"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/3-540-36576-1_27","volume-title":"Foundations of Software Science and Computational Structures","author":"C. Sprenger","year":"2003","unstructured":"Sprenger, C., Dam, M.: On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the \u03bc-Calculus. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 425\u2013440. Springer, Heidelberg (2003)"},{"key":"25_CR23","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C. Stirling","year":"1991","unstructured":"Stirling, C., Walker, D.: Local model checking in the modal \u03bc-calculus. Theoretical Computer Science\u00a089, 161\u2013177 (1991)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"25_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/jigpal\/12.1.1","volume":"12","author":"C.P. Wirth","year":"2004","unstructured":"Wirth, C.P.: Descente infinie + Deduction. Logic J. of the IGPL\u00a012(1), 1\u201396 (2004)","journal-title":"Logic J. of the IGPL"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35182-2_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T10:34:51Z","timestamp":1745404491000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35182-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642351815","9783642351822"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35182-2_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}