{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T12:41:11Z","timestamp":1760100071693},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-71070-7_35","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T05:56:30Z","timestamp":1219989390000},"page":"410-425","source":"Crossref","is-referenced-by-count":18,"title":["Deciding Effectively Propositional Logic Using DPLL and Substitution Sets"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"de Moura","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H.R. Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci.\u00a021, 317\u2013353 (1980)","journal-title":"J. Comput. Syst. Sci."},{"key":"35_CR2","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. In: [18], pp. 346\u2013361."},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11499107_4","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Dershowitz","year":"2005","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded Model Checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 408\u2013414. Springer, Heidelberg (2005)"},{"key":"35_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-62064-8_34","volume-title":"Perspectives of System Informatics","author":"A. Voronkov","year":"1996","unstructured":"Voronkov, A.: Merging relational database technology with constraint technology. In: Bjorner, D., Broy, M., Pottosin, I.V. (eds.) PSI 1996. LNCS, vol.\u00a01181, pp. 409\u2013419. Springer, Heidelberg (1996)"},{"key":"35_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/978-3-540-39715-1_10","volume-title":"Rules and Rule Markup Languages for the Semantic Web","author":"T. Tammet","year":"2003","unstructured":"Tammet, T., Kadarpik, V.: Combining an inference engine with database: A rule server. In: Schr\u00f6der, M., Wagner, G. (eds.) RuleML 2003. LNCS, vol.\u00a02876, pp. 136\u2013149. Springer, Heidelberg (2003)"},{"key":"35_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11575467_8","volume-title":"Programming Languages and Systems","author":"J. Whaley","year":"2005","unstructured":"Whaley, J., Avots, D., Carbin, M., Lam, M.S.: Using datalog with binary decision diagrams for program analysis. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 97\u2013118. Springer, Heidelberg (2005)"},{"key":"35_CR8","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(T). J. ACM\u00a053, 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"35_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74621-8_1","volume-title":"Frontiers of Combining Systems","author":"S. Krstic","year":"2007","unstructured":"Krstic, S., Goel, A.: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 1\u201327. Springer, Heidelberg (2007)"},{"key":"35_CR10","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.\u00a0172, 591\u2013632 (2008)","journal-title":"Artif. Intell."},{"key":"35_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1007\/11916277_39","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma learning in the model evolution calculus. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 572\u2013586. Springer, Heidelberg (2006)"},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"Baumgartner, P.: Logical engineering with instance-based methods. In: [18], pp. 404\u2013409.","DOI":"10.1007\/978-3-540-73595-3_30"},{"key":"35_CR13","first-page":"55","volume-title":"LICS","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: LICS, pp. 55\u201364. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"35_CR14","unstructured":"Gallo, G., Rago, G.: The satisfiability problem for the Sch\u00f6nfinkel-Bernays fragment: partial instantiation and hypergraph algorithms. Technical Report 4\/94, Dip. Informatica, Universit\u2018a di Pisa (1994)"},{"key":"35_CR15","doi-asserted-by":"crossref","unstructured":"Ferm\u00fcller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1791\u20131849. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50027-8"},{"key":"35_CR16","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Proof systems for effectively propositional logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008 (2008)"},{"key":"35_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11814771_28","volume-title":"Automated Reasoning","author":"H. Nivelle de","year":"2006","unstructured":"de Nivelle, H., Meng, J.: Geometric resolution: A proof procedure based on finite model search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 303\u2013317. Springer, Heidelberg (2006)"},{"key":"35_CR18","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-21","year":"2007","unstructured":"Pfenning, F. (ed.): CADE 2007. LNCS (LNAI), vol.\u00a04603. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T13:41:27Z","timestamp":1557754887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540710691","9783540710707"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}