{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:23:52Z","timestamp":1725798232782},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662441985"},{"type":"electronic","value":"9783662441992"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44199-2_47","type":"book-chapter","created":{"date-parts":[[2014,7,31]],"date-time":"2014-07-31T22:17:11Z","timestamp":1406845031000},"page":"303-306","source":"Crossref","is-referenced-by-count":1,"title":["Skolemization Modulo Theories"],"prefix":"10.1007","author":[{"given":"Konstantin","family":"Korovin","sequence":"first","affiliation":[]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"47_CR1","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press (1986)"},{"key":"47_CR2","doi-asserted-by":"crossref","unstructured":"Baaz, M., Egly, U., Leitsch, A.: Normal form transformations. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 5, pp. 273\u2013333. North Holland (2001)","DOI":"10.1016\/B978-044450813-3\/50007-2"},{"issue":"9","key":"47_CR3","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L. Moura De","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM\u00a054(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"47_CR4","unstructured":"Hodges, W.: Model theory. Cambridge Univ. Press (1995)"},{"key":"47_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-02959-2_14","volume-title":"Automated Deduction \u2013 CADE-22","author":"K. Korovin","year":"2009","unstructured":"Korovin, K.: Instantiation-based automated reasoning: From theory to practice. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 163\u2013166. Springer, Heidelberg (2009)"},{"key":"47_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"K. Korovin","year":"2013","unstructured":"Korovin, K.: Inst-gen \u2013 a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol.\u00a07797, pp. 239\u2013270. Springer, Heidelberg (2013)"},{"key":"47_CR7","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/BF01458217","volume":"76","author":"L. L\u00f6wenheim","year":"1915","unstructured":"L\u00f6wenheim, L.: \u00dcber M\u00f6glichkeiten im Relativkalk\u00fcl. Math. Annalen\u00a076, 447\u2013470 (1915)","journal-title":"Math. Annalen"},{"key":"47_CR8","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 6, pp. 335\u2013367. North Holland (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"47_CR9","unstructured":"Skolem, T.: Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit oder Beweisbarkeit mathematischer S\u00e4tze nebst einem Theoreme \u00fcber dichte Mengen. In: Skrifter utgitt av Videnskapsselskapet i Kristiania (1920)"},{"key":"47_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"628","DOI":"10.1007\/978-3-319-08867-9_42","volume-title":"CAV 2014","author":"M. Veanes","year":"2014","unstructured":"Veanes, M., Bj\u00f8rner, N., Nachmanson, L., Bereg, S.: Monadic decomposition. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 628\u2013645. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Software \u2013 ICMS 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44199-2_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T13:45:24Z","timestamp":1558964724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44199-2_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662441985","9783662441992"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44199-2_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}