{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:18:02Z","timestamp":1766135882922},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_35","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"476-491","source":"Crossref","is-referenced-by-count":9,"title":["Encoding First Order Proofs in SAT"],"prefix":"10.1007","author":[{"given":"Todd","family":"Deshane","sequence":"first","affiliation":[]},{"given":"Wenjin","family":"Hu","sequence":"additional","affiliation":[]},{"given":"Patty","family":"Jablonski","sequence":"additional","affiliation":[]},{"given":"Hai","family":"Lin","sequence":"additional","affiliation":[]},{"given":"Christopher","family":"Lynch","sequence":"additional","affiliation":[]},{"given":"Ralph Eric","family":"McGregor","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"35_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem Proving via General Matings. Journal of the Association for Computing Machinery\u00a028(2), 193\u2013214 (1981)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"35_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/10721959_16","volume-title":"Automated Deduction - CADE-17","author":"P. Baumgartner","year":"2000","unstructured":"Baumgartner, P.: FDPLL - A First-Order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol.\u00a01831, pp. 200\u2013219. Springer, Heidelberg (2000)"},{"key":"35_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. In: Baader, F. (ed.) Automated Deduction \u2013 CADE-19. LNCS (LNAI), vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"key":"35_CR4","unstructured":"Bell, J.L., Slomson, A.B.: Models and Ultraproducts, An Introduction, Dover (1969)"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science","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. Billon","year":"1996","unstructured":"Billon, J.: The Disconnection Method: a Confluent Integration of Unifications in the Analytic Framework. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"key":"35_CR6","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1015854101244","volume":"28","author":"V. Chandru","year":"2002","unstructured":"Chandru, V., Hooker, J., Rago, G., Shrivastava, A.: Partial Instantiation Methods For Inference in First-Order Logic. Journal of Automated Reasoning\u00a028, 371\u2013396 (2002)","journal-title":"Journal of Automated Reasoning"},{"issue":"7","key":"35_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, D., Loveland, D.: A Machine Program For Theorem Proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"35_CR8","unstructured":"Delaune, S., Lin, H., Lynch, C.: Protocol Verification Via Rigid\/Flexible Resolution (submitted 2007)"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT. Solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: 16th International Conference on Computer Aided Verification (CAV), Boston (USA) (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/3-540-57785-8_131","volume-title":"STACS 1994","author":"J. Goubault","year":"1994","unstructured":"Goubault, J.: The Complexity of Resource-Bounded First-Order Classical Logic. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol.\u00a0775, pp. 59\u201370. Springer, Heidelberg (1994)"},{"key":"35_CR12","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/B978-044450813-3\/50005-9","volume-title":"Handbook of Automated Reasoning, ch. 3","author":"R. H\u00e4hnle","year":"2001","unstructured":"H\u00e4hnle, R.: Tableaux and Related Methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 3, vol.\u00a01, pp. 101\u2013177. Elsevier, North-Holland (2001)"},{"key":"35_CR13","doi-asserted-by":"crossref","first-page":"2015","DOI":"10.1016\/B978-044450813-3\/50030-8","volume-title":"Handbook of Automated Reasoning, ch. 28","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Model Elimination and Connection Tableau Procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 28, 28th edn., vol.\u00a02, pp. 2015\u20132113. Elsevier, North-Holland (2001)","edition":"28"},{"key":"35_CR14","series-title":"Lecture Notes in Artificial Intelligence","first-page":"289","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Letz","year":"2005","unstructured":"Letz, R., Gernot, S.: Proof and Model Generation With Disconnection Tableaux. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 289\u2013306. Springer, Heidelberg (2005)"},{"key":"35_CR15","unstructured":"McCune, W.: A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems, Technical Report ANL\/MCS-TM-194, Argonne National Laboratory (1994)"},{"key":"35_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/11814948_28","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"S. Prestwich","year":"2006","unstructured":"Prestwich, S., Lynce, I.: Local Search for Unsatisfiability. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 283\u2013296. Springer, Heidelberg (2006)"},{"issue":"2-3","key":"35_CR17","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications, CASC\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications, CASC"},{"issue":"2","key":"35_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.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":"35_CR19","unstructured":"Stenz, G.: The Disconnection Tableaux, PhD thesis, TU M\u00fcnchen (2002)"},{"key":"35_CR20","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"Chang, C., Lee, C.R.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York and London (1973)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:09Z","timestamp":1619517189000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}