{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,21]],"date-time":"2023-06-21T11:31:24Z","timestamp":1687347084429},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/2.0"},{"start":{"date-parts":[[2009,7,23]],"date-time":"2009-07-23T00:00:00Z","timestamp":1248307200000},"content-version":"vor","delay-in-days":172,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/2.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2009,2]]},"DOI":"10.1007\/s10472-009-9150-9","type":"journal-article","created":{"date-parts":[[2009,7,22]],"date-time":"2009-07-22T10:23:19Z","timestamp":1248258199000},"page":"3-34","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Labelled splitting"],"prefix":"10.1007","volume":"55","author":[{"given":"Arnaud","family":"Fietzke","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,7,23]]},"reference":[{"key":"9150_CR1","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":"9150_CR2","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":"9150_CR3","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory, Third Kurt G\u00f6del Colloquium. LNCS, vol. 713","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.) Computational Logic and Proof Theory, Third Kurt G\u00f6del Colloquium. LNCS, vol. 713, pp. 83\u201396. Springer, New York (1993)"},{"key":"9150_CR4","volume-title":"Labelled Deduction","year":"2000","unstructured":"Basin, D., D\u2019Agostino, M., Gabbay, D.M., Matthews, S., Vigan\u00f3, L., (eds.) Labelled Deduction. Kluwer, Dordrecht (2000)"},{"issue":"4\u20135","key":"9150_CR5","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1016\/j.artint.2007.09.005","volume":"172","author":"P Baumgartner","year":"2008","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4\u20135), 591\u2013632 (2008)","journal-title":"Artif. Intell."},{"issue":"3","key":"9150_CR6","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 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"9150_CR7","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-45653-8_12","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001. LNAI, vol. 2250","author":"H de Nivelle","year":"2001","unstructured":"de\u00a0Nivelle, H.: Splitting through new proposition symbols. In: Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001. LNAI, vol. 2250, pp.\u00a0172\u2013185. Springer, New York (2001)"},{"key":"9150_CR8","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT solver. Theory and Applications of Satisfiability Testing, pp. 502\u2013518 (2004)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"9150_CR9","doi-asserted-by":"publisher","first-page":"1791","DOI":"10.1016\/B978-044450813-3\/50027-8","volume-title":"Handbook of Automated Reasoning, vol. II, chapter 25","author":"CG Ferm\u00fcller","year":"2001","unstructured":"Ferm\u00fcller, C.G., Leitsch, A., Hustadt, U., Tamet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0II, chapter\u00a025, pp.\u00a01791\u20131849. Elsevier, Amsterdam (2001)"},{"key":"9150_CR10","first-page":"459","volume-title":"4th International Joint Conference on Automated Reasoning (IJCAR). LNAI, vol. 5195","author":"A Fietzke","year":"2008","unstructured":"Fietzke, A., Weidenbach, C.: Labelled splitting. In: 4th International Joint Conference on Automated Reasoning (IJCAR). LNAI, vol. 5195, pp. 459\u2013474. Springer, New York (2008)"},{"key":"9150_CR11","unstructured":"Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research report MPI-I-2007-RG1-002, Max-Planck Institute for Informatics, Saarbr\u00fccken (2007)"},{"key":"9150_CR12","first-page":"311","volume-title":"21st International Conference on Automated Deduction (CADE-21). Lecture Notes in Computer Science, vol. 4603","author":"T Lev-Ami","year":"2007","unstructured":"Lev-Ami, T., Weidenbach, C., Reps, T., Sagiv, M.: Labelled clauses. In: 21st International Conference on Automated Deduction (CADE-21). Lecture Notes in Computer Science, vol. 4603, pp. 311\u2013327. Springer, New York (2007)"},{"key":"9150_CR13","first-page":"23","volume-title":"12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR\u201905. Lecture Notes in Computer Science, vol. 3835","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Decision procedures for SAT, SAT Modulo Theories and Beyond. The Barcelogic Tools. (Invited Paper). In: Sutcliffe, G., Voronkov, A. (eds.) 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR\u201905. Lecture Notes in Computer Science, vol. 3835, pp. 23\u201346. Springer, New York (2005)"},{"issue":"6","key":"9150_CR14","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. J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"9150_CR15","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning, vol. I, chapter 7","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, chapter\u00a07, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"key":"9150_CR16","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning, vol. 1, chapter 6","author":"A Nonnengart","year":"2001","unstructured":"Nonnengart, A. Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, chapter\u00a06, pp. 335\u2013367. Elsevier, Amsterdam (2001)"},{"key":"9150_CR17","unstructured":"Riazanov, A., Voronkov, A.: Splitting without backtracking. In: IJCAI, pp. 611\u2013617 (2001)"},{"issue":"2","key":"9150_CR18","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library: CNF release v1.2.1. J Autom Reason 21(2), 177\u2013203 (1998)","journal-title":"J Autom Reason"},{"key":"9150_CR19","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivations in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers on Computational Logic, vol.\u00a02, pp.\u00a0466\u2013483. Springer (1983). First published in: Studies in Constructive Mathematics and Mathematical Logic, (Slisenko, A.O., ed.) (1968)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"9150_CR20","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning, vol. 2, chapter 27","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, chapter\u00a027, pp. 1965\u20132012. Elsevier, Amsterdam (2001)"},{"key":"9150_CR21","first-page":"141","volume-title":"13th International Conference on Automated Deduction, CADE-13. LNAI, vol. 1104","author":"C Weidenbach","year":"1996","unstructured":"Weidenbach, C., Gaede, B., Rock, G.: Spass and flotter, version 0.42. In: McRobbie, M., Slaney, J. (eds.) 13th International Conference on Automated Deduction, CADE-13. LNAI, vol. 1104, pp.\u00a0141\u2013145. Springer, New York (1996)"},{"key":"9150_CR22","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"CADE-21: 21st International Conference on Automated Deduction. LNAI, vol. 4603","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-21: 21st International Conference on Automated Deduction. LNAI, vol. 4603, pp. 514\u2013520. Springer, New York (2007)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9150-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-009-9150-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9150-9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9150-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,31]],"date-time":"2021-08-31T20:28:10Z","timestamp":1630441690000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-009-9150-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":22,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["9150"],"URL":"https:\/\/doi.org\/10.1007\/s10472-009-9150-9","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2]]},"assertion":[{"value":"23 July 2009","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}