{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:43:40Z","timestamp":1749725020517},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_16","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"200-219","source":"Crossref","is-referenced-by-count":36,"title":["FDPLL \u2014 A First-Order Davis-Putnam-Logeman-Loveland Procedure"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-69778-0_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"P. Baumgartner","year":"1998","unstructured":"Baumgartner, P.: Hyper Tableaux \u2014 The Next Generation. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, p. 60. Springer, Heidelberg (1998)"},{"key":"16_CR2","unstructured":"Beckert, B.: Integration und Uniformierung von Methoden des tableaubasierten Theorembeweisens. Dissertation, University of Karlsruhe (1998)"},{"key":"16_CR3","first-page":"133","volume-title":"Automated Deduction. A Basis for Applications","author":"W. Bibel","year":"1998","unstructured":"Bibel, W., Br\u00fcning, S., Otten, J., Schaub, T.: Compressions and Extensions. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction. A Basis for Applications, vol.\u00a01, ch. 5, pp. 133\u2013179. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"16_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/3-540-48660-7_30","volume-title":"Automated Deduction - CADE-16","author":"P. Baumgartner","year":"1999","unstructured":"Baumgartner, P., Eisinger, N., Furbach, U.: A confluent connection calculus. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 329\u2013343. Springer, Heidelberg (1999)"},{"key":"16_CR5","series-title":"LNAI","volume-title":"Logics in Artificial Intelligence","author":"P. Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper Tableaux. In: Or\u0142owska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS (LNAI), vol.\u00a01126, Springer, Heidelberg (1996)"},{"key":"16_CR6","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/3-540-61208-4_8","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J.-P. Billon","year":"1996","unstructured":"Billon, J.-P.: The Disconnection Method. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Crawford, J.M., Auton, L.D.: Experimental results on the crossover point in random 3sat. Artificial Intelligence\u00a081 (1996)","DOI":"10.1016\/0004-3702(95)00046-1"},{"key":"16_CR8","volume-title":"Symbolic logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"Chang, C., Lee, R.: Symbolic logic and Mechanical Theorem Proving. Academic Press, London (1973)"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Caferra, R., Peltier, N.: Decision Procedures using Model Building techniques. In: Computer Science logic (CSL 1995) (1995)","DOI":"10.1007\/3-540-61377-3_35"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Davis, M.: Eliminating the irrelevant from mechanical proofs. In: Proceedings of Symposia in Applied Mathematics - Experimental Arithmetic, High Speed Computing and Mathematics, American Mathematical Society, vol.\u00a0XV, pp. 15\u201330 (1963)","DOI":"10.1090\/psapm\/015\/0170497"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Davis, M., Logeman, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05(7) (1962)","DOI":"10.1145\/368273.368557"},{"key":"16_CR12","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. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Eder, E.: Properties of Substitutions and Unifications. Journal of Symbolic Computation\u00a01(1) (March 1985)","DOI":"10.1016\/S0747-7171(85)80027-4"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-56992-8_10","volume-title":"Computer Science Logic","author":"C. Ferm\u00fcller","year":"1993","unstructured":"Ferm\u00fcller, C., Leitsch, A.: Model building by resolution. In: Martini, S., B\u00f6rger, E., Kleine B\u00fcning, H., J\u00e4ger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol.\u00a0702, pp. 134\u2013148. Springer, Heidelberg (1993)"},{"issue":"2","key":"16_CR15","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C. Ferm\u00fcller","year":"1996","unstructured":"Ferm\u00fcller, C., Leitsch, A.: Hyperresolution and automated model building. Journal of Logic and Computation\u00a06(2), 173\u2013230 (1996)","journal-title":"Journal of Logic and Computation"},{"key":"16_CR16","volume-title":"Proceedings of the 14th Symposium on Logic in Computer Science","author":"G. Gottlob","year":"1998","unstructured":"Gottlob, G., Pichler, R.: Working with Arms: Complexity Results on Atomic Representations of Herbrand Models. In: Proceedings of the 14th Symposium on Logic in Computer Science, IEEE, Los Alamitos (1998)"},{"key":"16_CR17","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"Lee, S.-J., Plaisted, D.: Eliminating Duplicates with the Hyper-Linking Strategy. Journal of Automated Reasoning\u00a09, 25\u201342 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 415\u2013434. Springer, Heidelberg (1988)","DOI":"10.1007\/BFb0012847"},{"issue":"2","key":"16_CR19","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/jigpal\/7.2.217","volume":"7","author":"N. Peltier","year":"1999","unstructured":"Peltier, N.: Pruning the search space and extracting more models in tableaux. Logic Journal of the IGPL\u00a07(2), 217\u2013251 (1999)","journal-title":"Logic Journal of the IGPL"},{"key":"16_CR20","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered Semantic Hyper Linking. In: Proceedings AAAI 1997 (1997)"},{"key":"16_CR21","series-title":"LNAI","first-page":"192","volume-title":"Automated Deduction - CADE-12","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 192\u2013206. Springer, Heidelberg (1994)"},{"key":"16_CR22","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An Efficient Propositional Theorem Prover. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:42:33Z","timestamp":1556019753000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/10721959_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}