{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T15:22:17Z","timestamp":1782400937398,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642397981","type":"print"},{"value":"9783642397998","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_30","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T23:13:06Z","timestamp":1373497986000},"page":"447-462","source":"Crossref","is-referenced-by-count":2,"title":["Combining Relational Learning with SMT Solvers Using CEGAR"],"prefix":"10.1007","author":[{"given":"Arun","family":"Chaganty","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Akash","family":"Lal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aditya V.","family":"Nori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sriram K.","family":"Rajamani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Principles of Programming Languages (POPL 2002), pp. 1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"issue":"5-6","key":"30_CR2","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The Software Model Checker Blast. STTT: International Journal on Software Tools for Technology Transfer\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT: International Journal on Software Tools for Technology Transfer"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Bilenko, M., Mooney, R.: Adaptive duplicate detection using learnable string similarity measures. In: Knowledge Discovery and Data Mining (KDD 2003), pp. 39\u201348 (2003)","DOI":"10.1145\/956750.956759"},{"key":"30_CR4","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer (2007)"},{"key":"30_CR5","unstructured":"Braz, R., Amir, E., Roth, D.: Lifted first-order probabilistic inference. In: International Joint Conference on Artificial Intelligence (IJCAI 2005), pp. 1319\u20131325 (2005)"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Kautz, H., Selman, B., Jiang, Y.: A general stochastic approach to solving problems with hard and soft constraints. In: Gu, D., Du, J., Pardalos, P. (eds.) The Satisfiability Problem: Theory and Applications, pp. 573\u2013586. AMS (1997)","DOI":"10.1090\/dimacs\/035\/15"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Kiddon, C., Domingos, P.: Coarse-to-fine inference and learning for first-order probabilistic models. In: National Conference on Artificial Intelligence, AAAI 2011 (2011)","DOI":"10.1609\/aaai.v25i1.8019"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Kok, S., Domingos, P.: Learning the structure of Markov logic networks. In: International Conference on Machine Learning (ICML 2005), pp. 441\u2013448 (2005)","DOI":"10.1145\/1102351.1102407"},{"key":"30_CR12","unstructured":"Kok, S., Sumner, M., Richardson, M., Singla, P., Poon, H., Lowd, D., Domingos, P.: The Alchemy system for statistical relational AI. Technical report, University of Washington (2007), http:\/\/alchemy.cs.washington.edu"},{"key":"30_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"Mihalkova, L., Mooney, R.: Bottom-up learning of Markov logic network structure. In: International Conference on Machine Learning (ICML 2007), pp. 625\u2013632 (2007)","DOI":"10.1145\/1273496.1273575"},{"key":"30_CR15","unstructured":"Milch, B., Zettlemoyer, L.S., Kersting, K., Haimes, M., Kaelbling, L.P.: Lifted probabilistic inference with counting formulas. In: National Conference on Artificial Intelligence (AAAI 2008), pp. 1062\u20131068 (2008)"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Niu, F., Re, C., Doan, A., Shavlik, J.: Tuffy: Scaling up statistical inference in Markov logic networks using an RDBMS. In: International Conference on Very Large Data Bases, VLDB 2011 (2011)","DOI":"10.14778\/1978665.1978669"},{"key":"30_CR17","unstructured":"Poole, D.: First-order probabilistic inference. In: International Joint Conference on Artificial Intelligence (IJCAI 2003), pp. 985\u2013991 (2003)"},{"key":"30_CR18","unstructured":"Poon, H., Domingos, P.: Joint inference in information extraction. In: National Conference on Artificial Intelligence (AAAI 2007), pp. 913\u2013918 (2007)"},{"key":"30_CR19","unstructured":"Poon, H., Domingos, P., Sumner, M.: A general method for reducing the complexity of relational inference and its application to mcmc. In: National Conference on Artificial Intelligence, AAAI 2008 (2008)"},{"key":"30_CR20","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10994-006-5833-1","volume":"62","author":"M. Richardson","year":"2006","unstructured":"Richardson, M., Domingos, P.: Markov logic networks. Machine Learning\u00a062, 107\u2013136 (2006)","journal-title":"Machine Learning"},{"key":"30_CR21","unstructured":"Riedel, S.: Cutting plane map inference for Markov logic. In: Statistical Relational Learning, SRL 2009 (2009)"},{"key":"30_CR22","unstructured":"Silberschatz, A., Korth, H., Sudarshan, S.: Database Systems Concepts, 5th edn. McGraw-Hill, Inc. (2006)"},{"key":"30_CR23","doi-asserted-by":"crossref","unstructured":"Singla, P., Domingos, P.: Entity resolution with Markov logic. In: International Conference on Data Mining (ICDM 2006), pp. 572\u2013582 (2006)","DOI":"10.1109\/ICDM.2006.65"},{"key":"30_CR24","unstructured":"Singla, P., Domingos, P.: Memory-efficient inference in relational domains. In: National Conference on Artificial Intelligence (AAAI 2006), pp. 488\u2013493 (2006)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,3]],"date-time":"2023-07-03T02:14:29Z","timestamp":1688350469000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}