{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T16:54:20Z","timestamp":1725555260519},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642130885"},{"type":"electronic","value":"9783642130892"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-13089-2_5","type":"book-chapter","created":{"date-parts":[[2010,5,7]],"date-time":"2010-05-07T12:05:27Z","timestamp":1273233927000},"page":"58-69","source":"Crossref","is-referenced-by-count":1,"title":["Complexity of the Satisfiability Problem for a Class of Propositional Schemata"],"prefix":"10.1007","author":[{"given":"Vincent","family":"Aravantinos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ricardo","family":"Caferra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Aravantinos, V., Caferra, R., Peltier, N.: A DPLL Proof Procedure For Propositional Iterated Schemata. In: Proceedings of the 21st European Summer School in Logic, Language and Information (Worskhop Structures and Deduction) (2009)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02716-1_4","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"V. Aravantinos","year":"2009","unstructured":"Aravantinos, V., Caferra, R., Peltier, N.: A Schemata Calculus For Propositional Logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol.\u00a05607, pp. 32\u201346. Springer, Heidelberg (2009)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-02716-1_8","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"D. Baelde","year":"2009","unstructured":"Baelde, D.: On the Proof Theory of Regular Fixed Points. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol.\u00a05607, pp. 93\u2013107. Springer, Heidelberg (2009)"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/S1570-2464(07)80015-2","volume-title":"Handbook of Modal Logic","author":"J. Bradfield","year":"2007","unstructured":"Bradfield, J., Stirling, C.: Modal Mu-Calculi. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, vol.\u00a03, pp. 721\u2013756. Elsevier Science Inc., New York (2007)"},{"key":"5_CR5","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":"5_CR6","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The Automation of Proof by Mathematical Induction. In: [14], pp. 845\u2013911","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"issue":"9","key":"5_CR7","first-page":"725","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"Cleaveland, R.: Tableau-based Model Checking in the Propositional Mu-calculus. Acta Inf.\u00a027(9), 725\u2013747 (1990)","journal-title":"Acta Inf."},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Comon, H.: Inductionless induction. In: [14], ch. 14","DOI":"10.1016\/B978-044450813-3\/50016-3"},{"key":"5_CR9","first-page":"27","volume":"7","author":"M. Fisher","year":"1974","unstructured":"Fisher, M., Rabin, M.: Super Exponential Complexity of presburger\u2019s Arithmetic. SIAM-AMS Proceedings\u00a07, 27\u201341 (1974)","journal-title":"SIAM-AMS Proceedings"},{"key":"5_CR10","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-94-017-1754-0_6","volume-title":"Handbook of Tableau Methods, ch. 6","author":"R. Gor\u00e9","year":"1999","unstructured":"Gor\u00e9, R.: Tableau Methods for Modal and Temporal Logics. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, ch. 6, pp. 297\u2013396. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"5_CR11","unstructured":"Hetzl, S., Leitsch, A., Weller, D., Paleo, B.W.: Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions. In: Sutcliffe, G., Colton, S., Schulz, S. (eds.) Workshop on Empirically Successful Automated Reasoning for Mathematics (ESARM), July 2008, pp. 21\u201341 (2008)"},{"key":"5_CR12","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Pu. Co., Reading (1979)"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/800070.802187","volume-title":"STOC \u201982: Proceedings of the fourteenth annual ACM symposium on Theory of computing","author":"N. Immerman","year":"1982","unstructured":"Immerman, N.: Relational Queries Computable in Polynomial Time (Extended Abstract). In: STOC \u201982: Proceedings of the fourteenth annual ACM symposium on Theory of computing, pp. 147\u2013152. ACM, New York (1982)"},{"key":"5_CR14","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol.\u00a02. Elsevier\/MIT Press (2001)"},{"key":"5_CR15","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 mu-Calculus. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 425\u2013440. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13089-2_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:54:42Z","timestamp":1619783682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13089-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642130885","9783642130892"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13089-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}