{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:02:45Z","timestamp":1767927765518,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642224379","type":"print"},{"value":"9783642224386","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","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-22438-6_17","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"207-221","source":"Crossref","is-referenced-by-count":13,"title":["Sort It Out with Monotonicity"],"prefix":"10.1007","author":[{"given":"Koen","family":"Claessen","sequence":"first","affiliation":[]},{"given":"Ann","family":"Lilliestr\u00f6m","sequence":"additional","affiliation":[]},{"given":"Nicholas","family":"Smallbone","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A., Coquand, T., Norell, U.: Connecting a logical framework to a first-order logic prover. In: Gramlich [7], pp. 285\u2013301","DOI":"10.1007\/11559306_17"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-14203-1_8","volume-title":"Automated Reasoning","author":"J.C. Blanchette","year":"2010","unstructured":"Blanchette, J.C., Krauss, A.: Monotonicity inference for higher-order formulas. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 91\u2013106. Springer, Heidelberg (2010)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Claessen, K., Lilliestr\u00f6m, A.: Automated inference of finite unsatisfiability. Journal of Automated Reasoning (2011), \n                  \n                    http:\/\/dx.doi.org\/10.1007\/s10817-010-9216-8\n                  \n                  \n                , doi: 10.1007\/s10817-010-9216-8","DOI":"10.1007\/s10817-010-9216-8"},{"key":"17_CR4","unstructured":"Claessen, K., S\u00f6rensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: Proc. of Workshop on Model Computation, MODEL (2003)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"17_CR6","volume-title":"A Mathematical Introduction to Logic, chap. 4.3 (Many-Sorted Logic)","author":"H.B. Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, ch. 4.3 (Many-Sorted Logic), 2nd edn. Academic Press, New York (2001)","edition":"2"},{"key":"17_CR7","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"5th International Workshop on Frontiers of Combining Systems, , FroCoS 2005, proceedings","year":"2005","unstructured":"Gramlich, B. (ed.): FroCos 2005. LNCS (LNAI), vol.\u00a03717. Springer, Heidelberg (2005)"},{"issue":"1","key":"17_CR8","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J. Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. Journal of Automated Reasoning\u00a040(1), 35\u201360 (2008)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"17_CR9","first-page":"73","volume":"5","author":"L.C. Paulson","year":"1999","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science\u00a05(3), 73\u201387 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich [7], pp. 48\u201364","DOI":"10.1007\/11559306_3"},{"issue":"4","key":"17_CR11","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"17_CR12","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BF00243005","volume":"5","author":"C.A. Wick","year":"1989","unstructured":"Wick, C.A., McCune, W.: Automated reasoning about elementary point-set topology. Journal of Automated Reasoning\u00a05(2), 239\u2013255 (1989)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T01:41:19Z","timestamp":1578534079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_17"}},"subtitle":["Translating between Many-Sorted and Unsorted First-Order Logic"],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}