{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:40:18Z","timestamp":1725518418964},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_39","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"459-474","source":"Crossref","is-referenced-by-count":2,"title":["Labelled Splitting"],"prefix":"10.1007","author":[{"given":"Arnaud","family":"Fietzke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"39_CR1","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM\u00a07, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"39_CR2","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL. Journal of the ACM\u00a053, 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"39_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory","author":"L. Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1993. LNCS, vol.\u00a0713, pp. 83\u201396. Springer, Heidelberg (1993)"},{"key":"39_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-61511-3_75","volume-title":"Automated Deduction - Cade-13","author":"C. Weidenbach","year":"1996","unstructured":"Weidenbach, C., Gaede, B., Rock, G.: Spass & flotter, version 0.42. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 141\u2013145. Springer, Heidelberg (1996)"},{"key":"39_CR5","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, pp. 1965\u20132012. Elsevier, Amsterdam (2001)"},{"key":"39_CR6","unstructured":"Fietzke, A., Weidenbach, C.: Labelled splitting. Research Report MPI-I-2008-RG1-001, Max-Planck Institute for Informatics, Saarbruecken, Germany (2008)"},{"key":"39_CR7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, pp. 19\u201399 (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"39_CR9","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"key":"39_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: System description: SPASS version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"},{"issue":"2","key":"39_CR11","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"39_CR12","unstructured":"Riazanov, A., Voronkov, A.: Splitting without backtracking. In: IJCAI, pp. 611\u2013617 (2001)"},{"volume-title":"Labelled deduction","year":"2000","key":"39_CR13","unstructured":"Basin, D., D\u2019Agostino, M., Gabbay, D.M., Matthews, S., Vigan\u00f3, L. (eds.): Labelled deduction. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"39_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-73595-3_21","volume-title":"Automated Deduction \u2013 CADE-21","author":"T. Lev-Ami","year":"2007","unstructured":"Lev-Ami, T., Weidenbach, C., Reps, T., Sagiv, M.: Labelled clauses. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 311\u2013327. Springer, Heidelberg (2007)"},{"key":"39_CR15","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT solver. Theory and Applications of Satisfiability Testing, 502\u2013518 (2004)","DOI":"10.1007\/978-3-540-24605-3_37"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:15:14Z","timestamp":1605762914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}