{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:58:21Z","timestamp":1725487101629},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540734437"},{"type":"electronic","value":"9783540734451"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73445-1_4","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T06:32:08Z","timestamp":1183444328000},"page":"38-52","source":"Crossref","is-referenced-by-count":4,"title":["Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps"],"prefix":"10.1007","author":[{"given":"Hicham","family":"Bensaid","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":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BFb0030608","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"A. Amaniss","year":"1997","unstructured":"Amaniss, A., Hermann, M., Lugiez, D.: Set operations for recurrent term schematizations. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 333\u2013344. Springer, Heidelberg (1997)"},{"issue":"1\u20133","key":"4_CR2","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0024-3795(94)00245-9","volume":"226\/228","author":"M. Bernstein","year":"1995","unstructured":"Bernstein, M., Sloane, N.J.A.: Some Canonical Sequences of Integers. Linear Algebra and its Applications\u00a0226\/228(1\u20133), 57\u201372 (1995)","journal-title":"Linear Algebra and its Applications"},{"key":"4_CR3","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, London, UK (1992)"},{"key":"4_CR4","series-title":"Applied Logic Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4020-2653-9","volume-title":"Automated Model Building","author":"R. Caferra","year":"2004","unstructured":"Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic Series, vol.\u00a031. Kluwer Academic Publishers, Boston (2004)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/3-540-54233-7_122","volume-title":"Automata, Languages and Programming","author":"H. Chen","year":"1991","unstructured":"Chen, H., Hsiang, J.: Logic programming with recurrence domains. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) Automata, Languages and Programming. LNCS, vol.\u00a0510, pp. 20\u201334. Springer, Heidelberg (1991)"},{"key":"4_CR6","first-page":"322","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"H. Comon","year":"1991","unstructured":"Comon, H.: Disunification: A survey. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 322\u2013359. MIT Press, Cambridge (1991)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch.\u00a014, pp. 913\u2013962. North-Holland (2001)","DOI":"10.1016\/B978-044450813-3\/50016-3"},{"key":"4_CR8","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_CR9","volume-title":"The Decision Problem, Solvable Classes of Quantificational Formulas","author":"B. Dreben","year":"1979","unstructured":"Dreben, B., Goldfarb, W.D.: The Decision Problem, Solvable Classes of Quantificational Formulas. Addison-Wesley, Reading (1979)"},{"issue":"1\u20132","key":"4_CR10","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_CR11","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1006\/jsco.1997.0114","volume":"24","author":"N. Peltier","year":"1997","unstructured":"Peltier, N.: Increasing the capabilities of model building by constraint solving with terms with integer exponents. Journal of Symbolic Computation\u00a024, 59\u2013101 (1997)","journal-title":"Journal of Symbolic Computation"},{"key":"4_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1007\/3-540-45744-5_48","volume-title":"Automated Reasoning","author":"N. Peltier","year":"2001","unstructured":"Peltier, N.: A General Method for Using Terms Schematizations in Automated Deduction. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 578\u2013593. Springer, Heidelberg (2001)"},{"key":"4_CR14","first-page":"153","volume":"5","author":"G.D. Plotkin","year":"1970","unstructured":"Plotkin, G.D.: A note on inductive generalization. Machine Intelligence\u00a05, 153\u2013163 (1970)","journal-title":"Machine Intelligence"},{"key":"4_CR15","first-page":"101","volume-title":"Machine Intelligence 6","author":"G.D. Plotkin","year":"1971","unstructured":"Plotkin, G.D.: A Further Note on Inductive Generalization. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 6, chapter 8, pp. 101\u2013124. Edinburgh University Press, Edinburgh (1971)"},{"key":"4_CR16","unstructured":"Schulz, S.: The E Equational Theorem Prover, \n                  \n                    http:\/\/www4.informatik.tu-muenchen.de\/~schulz\/WORK\/eprover.html"},{"key":"4_CR17","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1613\/jair.275","volume":"4","author":"T. Walsh","year":"1996","unstructured":"Walsh, T.: A divergence critic for inductive proof. Journal of Artificial Intelligence Research\u00a04, 209\u2013235 (1996)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"4_CR18","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)"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73445-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T16:52:58Z","timestamp":1550422378000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73445-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540734437","9783540734451"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73445-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}