{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:36:36Z","timestamp":1771025796291,"version":"3.50.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319409696","type":"print"},{"value":"9783319409702","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40970-2_20","type":"book-chapter","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T07:14:55Z","timestamp":1465542895000},"page":"323-341","source":"Crossref","is-referenced-by-count":14,"title":["Finding Finite Models in Multi-sorted First-Order Logic"],"prefix":"10.1007","author":[{"given":"Giles","family":"Reger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"20_CR1","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). http:\/\/www.SMT-LIB.org"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/978-3-642-36742-7_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 493\u2013507. Springer, Heidelberg (2013)"},{"issue":"2","key":"20_CR3","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/s10817-010-9216-8","volume":"47","author":"K Claessen","year":"2011","unstructured":"Claessen, K., Lilliestr\u00f6m, A.: Automated inference of finite unsatisfiability. J. Autom. Reasoning 47(2), 111\u2013132 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/978-3-642-22438-6_17","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Claessen","year":"2011","unstructured":"Claessen, K., Lilliestr\u00f6m, A., Smallbone, N.: Sort it out with monotonicity. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 207\u2013221. Springer, Heidelberg (2011)"},{"key":"20_CR5","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style model finding. In: CADE-19 Workshop: Model Computation - Principles, Algorithms and Applications (2003)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"4","key":"20_CR8","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-25324-9_1","volume-title":"Advances in Artificial Intelligence","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Case studies on invariant generation using a saturation theorem prover. In: Batyrshin, I., Sidorov, G. (eds.) MICAI 2011, Part I. LNCS, vol. 7094, pp. 1\u201315. Springer, Heidelberg (2011)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013)"},{"key":"20_CR12","unstructured":"Mccune, W.: A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems. Technical report, Argonne National Laboratory (1994)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"640","DOI":"10.1007\/978-3-642-39799-8_42","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640\u2013655. Springer, Heidelberg (2013)"},{"key":"20_CR14","unstructured":"Schulz, S.: A comparison of different techniques for grounding near-propositional CNF formulae. In: Proceedings of the Fifteenth International Florida Artificial Intelligence Research Society Conference, May 14\u201316, 2002, Pensacola Beach, Florida, USA, pp. 72\u201376 (2002)"},{"key":"20_CR15","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec, a cross community logic solving service (2012). https:\/\/www.starexec.org"},{"issue":"4","key":"20_CR16","doi-asserted-by":"crossref","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. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"2","key":"20_CR17","first-page":"199","volume":"18","author":"T Tammet","year":"1997","unstructured":"Tammet, T.: Reasoning. Gandalf. J. Autom 18(2), 199\u2013204 (1997)","journal-title":"Gandalf. J. Autom"},{"key":"20_CR18","unstructured":"Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI 95, Montr\u00e9al Qu\u00e9bec, Canada, August 20\u201325 1995, vol. 2s, pp. 298\u2013303 (1995)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40970-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:06:04Z","timestamp":1498305964000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40970-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409696","9783319409702"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40970-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}