{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:04Z","timestamp":1725490864684},"publisher-location":"Berlin, Heidelberg","reference-count":61,"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_30","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T05:31:33Z","timestamp":1188451893000},"page":"404-409","source":"Crossref","is-referenced-by-count":11,"title":["Logical Engineering with Instance-Based Methods"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"30_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, pp. 60\u201376. Springer, Heidelberg (1998)"},{"key":"30_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 \u2013 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":"30_CR3","volume-title":"AI in the new Millenium","author":"P. Baumgartner","year":"2002","unstructured":"Baumgartner, P.: A First-Order Logic Davis-Putnam-Logemann-Loveland Procedure. In: Lakemeyer, G., Nebel, B. (eds.) AI in the new Millenium, Morgan Kaufmann, Seattle (2002)"},{"key":"30_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.) Automated Deduction - CADE-16. LNCS (LNAI), vol.\u00a01632, pp. 329\u2013343. Springer, Heidelberg (1999)"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. Journal of Applied Logic (to appear)","DOI":"10.1016\/j.jal.2007.07.005"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","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, vol.\u00a01126, Springer, Heidelberg (1996)"},{"issue":"1","key":"30_CR7","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218213006002552","volume":"15","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. International Journal of Artificial Intelligence Tools\u00a015(1), 21\u201352 (2006)","journal-title":"International Journal of Artificial Intelligence Tools"},{"key":"30_CR8","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":"30_CR9","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.-P. Billon","year":"1996","unstructured":"Billon, J.-P.: The Disconnection Method. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"key":"30_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_11","volume-title":"Automated Reasoning","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Schmidt, R.: Blocking and other enhancements for bottom-up model generation methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"30_CR11","series-title":"LNAI","volume-title":"Proc. 6th European Workshop on Logics in AI (JELIA)","author":"F. Bry","year":"1998","unstructured":"Bry, F., Torge, S.: A Deduction Method Complete for Refutation and Finite Satisfiability. In: Proc. 6th European Workshop on Logics in AI (JELIA). LNCS (LNAI), Springer, Heidelberg (1998)"},{"key":"30_CR12","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":"30_CR13","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus with equality. In: Nieuwenhuis [Nie05], pp. 392\u2013408","DOI":"10.1007\/11532231_29"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-12","year":"1994","unstructured":"Bundy, A. (ed.): Automated Deduction - CADE-12. LNCS, vol.\u00a0814. Springer, Heidelberg (1994)"},{"key":"30_CR15","unstructured":"Chinlund, T.J., Davis, M., Hinman, P.G., McIlroy, M.D.: Theorem-Proving by Matching. Technical report, Bell Laboratories (1964)"},{"key":"30_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"628","DOI":"10.1007\/978-3-540-30227-8_52","volume-title":"Logics in Artificial Intelligence","author":"M. Cadoli","year":"2004","unstructured":"Cadoli, M., Mancini, T.: Exploiting functional dependencies in declarative problem specifications. In: Alferes, J.J., Leite, J.A. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 628\u2013640. Springer, Heidelberg (2004)"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Cadoli, M., Mancini, T.: Using a theorem prover for reasoning on constraint problems. In: AI*IA, pp. 38\u201349 (2005)","DOI":"10.1007\/11558590_4"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Chu, H., Plaisted, D.A.: Semantically Guided First-Order Theorem Proving using Hyper-Linking. In: Bundy [Bun94], pp. 192\u2013206","DOI":"10.1007\/3-540-58156-1_14"},{"key":"30_CR19","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-19","author":"K. Claessen","year":"2003","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve mace-style finite model building. In: Baader, F. (ed.) Automated Deduction \u2013 CADE-19. LNCS (LNAI), vol.\u00a02741, Springer, Heidelberg (2003)"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Davis, M.: Eliminating the irrelevant from mechanical proofs. In: Proceedings of Symposia in Applied Amthematics \u2013 Experimental Arithmetic, High Speed Computing and Mathematics, vol. XV, pp. 15\u201330. American Mathematical Society (1963)","DOI":"10.1090\/psapm\/015\/0170497"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5(7) (1962)","DOI":"10.1145\/368273.368557"},{"issue":"7","key":"30_CR22","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"30_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"},{"issue":"3","key":"30_CR24","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(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"30_CR25","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","year":"2002","unstructured":"Egly, U., Ferm\u00fcller, C.G. (eds.): TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381. Springer, Heidelberg (2002)"},{"issue":"2","key":"30_CR26","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. J. Log. Comput.\u00a06(2), 173\u2013203 (1996)","journal-title":"J. Log. Comput."},{"key":"30_CR27","doi-asserted-by":"crossref","first-page":"1791","DOI":"10.1016\/B978-044450813-3\/50027-8","volume-title":"Handbook of Automated Reasoning, ch. 25","author":"C.G. Ferm\u00fcller","year":"2001","unstructured":"Ferm\u00fcller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 25, 25th edn., vol.\u00a0II, pp. 1791\u20131849. Elsevier, North-Holland (2001)","edition":"25"},{"key":"30_CR28","doi-asserted-by":"crossref","unstructured":"Ferm\u00fcller, C.G., Pichler, R.: Model representation via contexts and implicit generalizations. In: Nieuwenhuis [Nie05], pp. 409\u2013423","DOI":"10.1007\/11532231_30"},{"key":"30_CR29","doi-asserted-by":"crossref","unstructured":"Georgieva, L., Hustadt, U., Schmidt, R.A.: Hyperresolution for guarded formulae. Journal of Symbolic Computation (2002)","DOI":"10.1016\/S0747-7171(03)00034-8"},{"key":"30_CR30","unstructured":"Ganzinger, H., Korovin, K.: New directions in instance-based theorem proving. In: LICS - Logics in Computer Science (2003)"},{"key":"30_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/978-3-540-30124-0_9","volume-title":"Computer Science Logic","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 71\u201384. Springer, Heidelberg (2004)"},{"key":"30_CR32","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Ganzinger","year":"2006","unstructured":"Ganzinger, H., Korovin, K.: Theory Instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, Springer, Heidelberg (2006)"},{"issue":"4","key":"30_CR33","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1015854101244","volume":"28","author":"J.N. Hooker","year":"2002","unstructured":"Hooker, J.N., Rago, G., Chandru, V., Shrivastava, A.: Partial Instantiation Methods for Inference in First Order Logic. Journal of Automated Reasoning\u00a028(4), 371\u2013396 (2002)","journal-title":"Journal of Automated Reasoning"},{"issue":"1-3","key":"30_CR34","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10817-006-9046-x","volume":"38","author":"S. Jacobs","year":"2007","unstructured":"Jacobs, S., Waldmann, U.: Comparing instance generation methods for automated reasoning. J. Autom. Reason.\u00a038(1-3), 57\u201378 (2007)","journal-title":"J. Autom. Reason."},{"key":"30_CR35","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":"30_CR36","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45653-8_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Proof and Model Generation with Disconnection Tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, Springer, Heidelberg (2001)"},{"key":"30_CR37","doi-asserted-by":"crossref","unstructured":"Letz, R., Stenz, G.: Integration of Equality Reasoning into the Disconnection Calculus. In: Egly and Ferm\u00fcller [EF02], pp. 176\u2013190","DOI":"10.1007\/3-540-45616-3_13"},{"issue":"1-3","key":"30_CR38","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10817-006-9048-8","volume":"38","author":"R. Letz","year":"2007","unstructured":"Letz, R., Stenz, G.: The disconnection tableau calculus. J. Autom. Reason.\u00a038(1-3), 79\u2013126 (2007)","journal-title":"J. Autom. Reason."},{"key":"30_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"CADE-9","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) CADE-9. LNCS, vol.\u00a0310, pp. 415\u2013434. Springer, Heidelberg (1988)"},{"key":"30_CR40","unstructured":"McCune, W.: A davis-putnam program and its application to finite first-order model search: Qusigroup existence problems. Technical report, Argonne National Laboratory (1994)"},{"issue":"1-3","key":"30_CR41","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/S0743-1066(98)10004-3","volume":"37","author":"F. Mesnard","year":"1998","unstructured":"Mesnard, F., Hoarau, S., Maillard, A.: CLP(\u03c7) for automatically proving program properties. J. Log. Program\u00a037(1-3), 77\u201393 (1998)","journal-title":"J. Log. Program"},{"key":"30_CR42","first-page":"549","volume-title":"International Semantic Web Conference","author":"B. Motik","year":"2004","unstructured":"Motik, B., Sattler, U., Studer, R.: Query answering for owl-dl with rules. In: Dubois, D., Welty, C.A., Williams, M.-A. (eds.) International Semantic Web Conference, pp. 549\u2013563. AAAI Press, Stanford (2004)"},{"key":"30_CR43","unstructured":"Mitchell, D., Ternovska, E., Hach, F., Mohebali, R.: Model expansion as a framework for modelling and solving search problems. Technical Report TR 2006-24 (December 2006)"},{"key":"30_CR44","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","year":"2005","unstructured":"Nieuwenhuis, R. (ed.): Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632. Springer, Heidelberg (2005)"},{"issue":"6","key":"30_CR45","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-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"issue":"5","key":"30_CR46","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1093\/logcom\/7.5.581","volume":"7","author":"H.J. Ohlbach","year":"1997","unstructured":"Ohlbach, H.J., Schmidt, R.A.: Functional translation and second-order frame properties of modal logics. Journal of Logic and Computation\u00a07(5), 581\u2013603 (1997)","journal-title":"Journal of Logic and Computation"},{"issue":"1-2","key":"30_CR47","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0747-7171(03)00027-0","volume":"36","author":"N. Peltier","year":"2003","unstructured":"Peltier, N.: A calculus combining resolution and enumeration for building finite models. Journal of Symbolic Computation\u00a036(1-2), 49\u201377 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"30_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/978-3-540-45206-5_15","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"N. Peltier","year":"2003","unstructured":"Peltier, N.: A more efficient tableaux procedure for simultaneous search for refutations and finite models. In: Mayer, M.C., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol.\u00a02796, pp. 181\u2013195. Springer, Heidelberg (2003)"},{"key":"30_CR49","unstructured":"Plaisted, D.A., Lee, S.-J.: Inference by clause matching. In: Ras, Z.W., Zemankova, M. (eds.) Intelligent Systems: State of the Art and Future Directions, pp. 200\u2013235. Ellis Horwood, New York (1990)"},{"key":"30_CR50","doi-asserted-by":"crossref","unstructured":"Plaisted, D.: The Search Efficiency of Theorem Proving Strategies. In: Bundy [Bun94]","DOI":"10.1007\/3-540-58156-1_5"},{"key":"30_CR51","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered Semantic Hyper Linking. In: Proceedings of Fourteenth National Conference on Artificial Intelligence (AAAI-1997) (1997)"},{"issue":"3","key":"30_CR52","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D.A. Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered Semantic Hyper Linking. Journal of Automated Reasoning\u00a025(3), 167\u2013217 (2000)","journal-title":"Journal of Automated Reasoning"},{"issue":"6","key":"30_CR53","first-page":"71","volume":"21","author":"S. Ranise","year":"2006","unstructured":"Ranise, S., Tinelli, C.: Satisfiability modulo theories. Trends and Controversies - IEEE Intelligent Systems Magazine\u00a021(6), 71\u201381 (2006)","journal-title":"Trends and Controversies - IEEE Intelligent Systems Magazine"},{"issue":"4","key":"30_CR54","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1023\/A:1006043519663","volume":"22","author":"R.A. Schmidt","year":"1999","unstructured":"Schmidt, R.A.: Decidability by resolution for propositional modal logics. J. Autom. Reason.\u00a022(4), 379\u2013396 (1999)","journal-title":"J. Autom. Reason."},{"key":"30_CR55","doi-asserted-by":"crossref","unstructured":"Schmidt, R.A., Hustadt, U.: The axiomatic translation principle for modal logic. ACM Transactions on Computational Logic (to appear)","DOI":"10.1145\/1276920.1276921"},{"key":"30_CR56","series-title":"Lecture Notes in Artificial Intelligence","first-page":"289","volume-title":"Automated Reasoning","author":"G. Stenz","year":"2004","unstructured":"Stenz, G., Letz, R.: Generlized handling of variables in disconnection tableaux. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 289\u2013306. Springer, Heidelberg (2004)"},{"key":"30_CR57","unstructured":"Slaney, J.: Finder (finite domain enumerator): Notes and guide. Technical Report TR-ARP-1\/92, Australian National University, Automated Reasoning Project, Canberra (1992)"},{"issue":"2","key":"30_CR58","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":"30_CR59","doi-asserted-by":"crossref","unstructured":"Stenz, G.: DCTP 1.2 - System Abstract. In: Egly and Ferm\u00fcller [BF02], pp. 335\u2013340","DOI":"10.1007\/3-540-45616-3_24"},{"key":"30_CR60","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45757-7_26","volume-title":"Logics in Artificial Intelligence","author":"C. Tinelli","year":"2002","unstructured":"Tinelli, C.: A DPLL-based calculus for ground satisfiability modulo theories. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol.\u00a02424, Springer, Heidelberg (2002)"},{"key":"30_CR61","unstructured":"Zhang, J., Zhang, H.: Sem: a system for enumerating models. In: IJCAI-1995 \u2014 Proceedings of the 14 th International Joint Conference on Artificial Intelligence, Montreal, pp. 298\u2013303 (1995)"}],"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_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:53:08Z","timestamp":1619502788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}