{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:57:20Z","timestamp":1725533840283},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027154"},{"type":"electronic","value":"9783642027161"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02716-1_4","type":"book-chapter","created":{"date-parts":[[2009,6,30]],"date-time":"2009-06-30T00:22:21Z","timestamp":1246321341000},"page":"32-46","source":"Crossref","is-referenced-by-count":14,"title":["A Schemata Calculus for Propositional Logic"],"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":[{"issue":"2","key":"4_CR1","doi-asserted-by":"publisher","first-page":"219","DOI":"10.2178\/bsl\/1146620060","volume":"12","author":"J. Corcoran","year":"2006","unstructured":"Corcoran, J.: Schemata: the concept of schema in the history of logic. The Bulletin of Symbolic Logic\u00a012(2), 219\u2013240 (2006)","journal-title":"The Bulletin of Symbolic Logic"},{"unstructured":"Kneale, W., Kneale, M.: The development of logic. Clarendon Press, Oxford University Press (1986)","key":"4_CR2"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BFb0049322","volume-title":"Computer Science Logic","author":"M. Baaz","year":"1994","unstructured":"Baaz, M., Zach, R.: Short proofs of tautologies using the schema of equivalence. In: Meinke, K., B\u00f6rger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol.\u00a0832, pp. 33\u201335. Springer, Heidelberg (1994)"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"29","DOI":"10.2307\/1996581","volume":"177","author":"R.J. Parikh","year":"1973","unstructured":"Parikh, R.J.: Some results on the length of proofs. Transactions of the American Mathematical Society\u00a0177, 29\u201336 (1973)","journal-title":"Transactions of the American Mathematical Society"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(98)00304-1","volume":"224","author":"M. Baaz","year":"1999","unstructured":"Baaz, M.: Note on the generalization of calculations. Theoretical Computer Science\u00a0224, 3\u201311 (1999)","journal-title":"Theoretical Computer Science"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF01625836","volume":"27","author":"J. Kraj\u00ed\u010dek","year":"1988","unstructured":"Kraj\u00ed\u010dek, J., Pudl\u00e1k, P.: The number of proof lines and the size of proofs in first order logic. Archive for Mathematical Logic\u00a027, 69\u201384 (1988)","journal-title":"Archive for Mathematical Logic"},{"issue":"2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1610","DOI":"10.1007\/BF01098278","volume":"55","author":"V.P. Orevkov","year":"1991","unstructured":"Orevkov, V.P.: Proof schemata in Hilbert-type axiomatic theories. Journal of Mathematical Sciences\u00a055(2), 1610\u20131620 (1991)","journal-title":"Journal of Mathematical Sciences"},{"key":"4_CR8","volume-title":"Automated Reasoning, Introduction and Applications","author":"L. Wos","year":"1992","unstructured":"Wos, L., Overbeek, R., Lusk, E., Boyle, J.: Automated Reasoning, Introduction and Applications, 2nd edn. McGraw-Hill, New York (1992)","edition":"2"},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"2351","DOI":"10.1098\/rsta.2005.1650","volume":"363","author":"H. Barendregt","year":"2005","unstructured":"Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Philosophical Transactions of the Royal Society A\u00a0363, 2351\u20132375 (2005)","journal-title":"Philosophical Transactions of the Royal Society A"},{"key":"4_CR10","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1988","unstructured":"Wos, L.: Automated Reasoning: 33 Basic Research Problems. Prentice-Hall, Englewood Cliffs (1988)"},{"issue":"1\u20132","key":"4_CR11","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/S0304-3975(96)00052-7","volume":"176","author":"M. Hermann","year":"1997","unstructured":"Hermann, M., Galbav\u00fd, R.: Unification of Infinite Sets of Terms schematized by Primal Grammars. Theoretical Computer Science\u00a0176(1\u20132), 111\u2013158 (1997)","journal-title":"Theoretical Computer Science"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/3-540-54303-1","volume-title":"Conditional and Typed Rewriting Systems","author":"H. Chen","year":"1991","unstructured":"Chen, H., Hsiang, J., Kong, H.: On finite representations of infinite sequences of terms. In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol.\u00a0516, pp. 100\u2013114. Springer, Heidelberg (1991)"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/BF01294596","volume":"28","author":"H. Comon","year":"1995","unstructured":"Comon, H.: On unification of terms with integer exponents. Mathematical System Theory\u00a028, 67\u201388 (1995)","journal-title":"Mathematical System Theory"},{"key":"4_CR14","volume-title":"A computational logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A computational logic. Academic Press, London (1979)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/BFb0013087","volume-title":"Logic Programming and Automated Reasoning","author":"A. Bouhoula","year":"1992","unstructured":"Bouhoula, A., Kounalis, E., Rusinowitch, M.: SPIKE, an automatic theorem prover. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 460\u2013462. Springer, Heidelberg (1992)"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1016\/B978-044450813-3\/50016-3","volume-title":"Handbook of Automated Reasoning","author":"H. Comon","year":"2001","unstructured":"Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 913\u2013962. North-Holland, Amsterdam (2001)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"647","DOI":"10.1007\/3-540-52885-7_123","volume-title":"10th International Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam system. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 647\u2013648. Springer, Heidelberg (1990)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11554554_20","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Stratulat","year":"2005","unstructured":"Stratulat, S.: Automatic \u2018Descente Infinie\u2019 Induction Reasoning. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS, vol.\u00a03702, pp. 262\u2013276. Springer, Heidelberg (2005)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-60381-6_21","volume-title":"Conditional and Typed Rewriting Systems","author":"C.P. Wirth","year":"1995","unstructured":"Wirth, C.P., Becker, K.: Abstract notions and inference systems for proofs by mathematical induction. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, pp. 353\u2013373. Springer, Heidelberg (1995)"},{"key":"4_CR20","first-page":"825","volume-title":"Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications","author":"C. Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, February 2009, vol.\u00a0185, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"issue":"2","key":"4_CR21","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation\u00a0183(2), 140\u2013164 (2003)","journal-title":"Information and Computation"},{"key":"4_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968)"},{"key":"4_CR23","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1990","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, Heidelberg (1990)"},{"unstructured":"Cooper, D.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 91\u201399. Edinburgh University Press (1972)","key":"4_CR24"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02716-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:27:00Z","timestamp":1558268820000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02716-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027154","9783642027161"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02716-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}