{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:57:25Z","timestamp":1725533845014},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027154"},{"type":"electronic","value":"9783642027161"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02716-1_8","type":"book-chapter","created":{"date-parts":[[2009,6,30]],"date-time":"2009-06-30T04:22:21Z","timestamp":1246335741000},"page":"93-107","source":"Crossref","is-referenced-by-count":4,"title":["On the Proof Theory of Regular Fixed Points"],"prefix":"10.1007","author":[{"given":"David","family":"Baelde","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Baelde, D.: A linear approach to the proof-theory of least and greatest fixed points. PhD thesis, Ecole Polytechnique (December 2008)"},{"key":"8_CR2","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-540-73595-3_28","volume-title":"Automated Deduction \u2013 CADE-21","author":"D. Baelde","year":"2007","unstructured":"Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 391\u2013397. Springer, Heidelberg (2007)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-540-75560-9_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Baelde","year":"2007","unstructured":"Baelde, D., Miller, D.: Least and greatest fixed points in linear logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol.\u00a04790, pp. 92\u2013106. Springer, Heidelberg (2007)"},{"key":"8_CR4","series-title":"LNAI","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":"8_CR5","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"Cleaveland, R.: Tableau-based model checking in the propositional mu-calculus. Acta Informatica\u00a027, 725\u2013747 (1990)","journal-title":"Acta Informatica"},{"key":"8_CR6","unstructured":"Girard, J.-Y.: A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu (February 1992)"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R. McDowell","year":"2000","unstructured":"McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoretical Computer Science\u00a0232, 91\u2013119 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"8_CR8","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D. Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. on Computational Logic\u00a06(4), 749\u2013783 (2005)","journal-title":"ACM Trans. on Computational Logic"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-3-540-24849-1_19","volume-title":"Types for Proofs and Programs","author":"A. Momigliano","year":"2004","unstructured":"Momigliano, A., Tiu, A.: Induction and co-induction in sequent calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 293\u2013308. Springer, Heidelberg (2004)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-45931-6_25","volume-title":"Foundations of Software Science and Computation Structures","author":"L. Santocanale","year":"2002","unstructured":"Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 357\u2013371. Springer, Heidelberg (2002)"},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1109\/LICS.1993.287585","volume-title":"Eighth Annual Symposium on Logic in Computer Science","author":"P. Schroeder-Heister","year":"1993","unstructured":"Schroeder-Heister, P.: Rules of definitional reflection. In: Vardi, M. (ed.) Eighth Annual Symposium on Logic in Computer Science, June 1993, pp. 222\u2013232. IEEE Computer Society Press, IEEE, Los Alamitos (1993)"},{"key":"8_CR12","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. Spenger","year":"2003","unstructured":"Spenger, C., Dams, 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":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11539452_7","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A. Tiu","year":"2005","unstructured":"Tiu, A.: Model checking for \u03c0-calculus using proof search. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 36\u201350. Springer, Heidelberg (2005)"},{"key":"8_CR14","unstructured":"Tiu, A., Nadathur, G., Miller, D.: Mixing finite success and finite failure in an automated prover. In: Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL 2005), December 2005, pp. 79\u201398 (2005)"}],"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-642-02716-1_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T10:55:56Z","timestamp":1619780156000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02716-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027154","9783642027161"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02716-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}