{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T12:27:29Z","timestamp":1743078449870,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642210426"},{"type":"electronic","value":"9783642210433"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21043-3_2","type":"book-chapter","created":{"date-parts":[[2011,5,24]],"date-time":"2011-05-24T16:36:15Z","timestamp":1306254975000},"page":"13-25","source":"Crossref","is-referenced-by-count":2,"title":["Grounding Formulas with Complex Terms"],"prefix":"10.1007","author":[{"given":"Amir","family":"Aavani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiongnan","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eugenia","family":"Ternovska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Mitchell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Frisch, A.M., Grum, M., Jefferson, C., Hernandez, B.M., Miguel, I.: The design of ESSENCE: a constraint language for specifying combinatorial problems. In: Proc. IJCAI 2007 (2007)"},{"key":"2_CR2","unstructured":"Mitchell, D., Ternovska, E.: A framework for representing and solving NP search problems. In: Proc. AAAI 2005 (2005)"},{"key":"2_CR3","first-page":"98","volume-title":"ECAI 2006: 17th European Conference on Artificial Intelligence, Proceedings Including Prestigious Applications of Intelligent Systems (PAIS 2006)","author":"I. Gent","year":"2006","unstructured":"Gent, I., Jefferson, C., Miguel, I.: Minion: A fast, scalable, constraint solver. In: ECAI 2006: 17th European Conference on Artificial Intelligence, Proceedings Including Prestigious Applications of Intelligent Systems (PAIS 2006), Riva del Garda, Italy, August 29-September 1, vol.\u00a098, p. 98. Ios Pr. Inc., Amsterdam (2006)"},{"key":"2_CR4","unstructured":"Patterson, M., Liu, Y., Ternovska, E., Gupta, A.: Grounding for model expansion in k-guarded formulas with inductive definitions. In: Proc. IJCAI 2007, pp. 161\u2013166 (2007)"},{"key":"2_CR5","unstructured":"Mohebali, R.: A method for solving NP search based on model expansion and grounding. Master\u2019s thesis, Simon Fraser University (2006)"},{"issue":"115-125","key":"2_CR6","first-page":"10","volume":"2","author":"G. Tseitin","year":"1968","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in constructive mathematics and mathematical logic\u00a02(115-125), 10\u201313 (1968)","journal-title":"Studies in constructive mathematics and mathematical logic"},{"key":"2_CR7","volume-title":"AAAI","author":"I. Lynce","year":"2006","unstructured":"Lynce, I., Marques-Silva, J.: Efficient haplotype inference with boolean satisfiability. In: AAAI. AAAI Press, Menlo Park (2006)"},{"key":"2_CR8","unstructured":"Rendl, A.: Effective compilation of constraint models (2010)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-540-74970-7_38","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"N. Nethercote","year":"2007","unstructured":"Nethercote, N., Stuckey, P., Becket, R., Brand, S., Duck, G., Tack, G.: MiniZinc: Towards a standard CP modelling language. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 529\u2013543. Springer, Heidelberg (2007)"},{"key":"2_CR10","unstructured":"Wittocx, J., Mari\u00ebn, M., De Pooter, S.: The idp system (2008), Obtainable via www.cs.kuleuven.be\/dtai\/krr\/software.html"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Wittocx, J.: Finite domain and symbolic inference methods for extensions of first-order logic. AI Communications (2010) (accepted)","DOI":"10.3233\/AIC-2010-0474"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-02777-2_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"R. As\u00edn","year":"2009","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality Networks and Their Applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 167\u2013180. Springer, Heidelberg (2009)"},{"key":"2_CR13","unstructured":"E\u00e9n, N.: SAT Based Model Checking. PhD thesis (2005)"}],"container-title":["Lecture Notes in Computer Science","Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21043-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,19]],"date-time":"2020-06-19T13:31:05Z","timestamp":1592573465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21043-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642210426","9783642210433"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21043-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}