{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:38Z","timestamp":1760202638203},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642308840"},{"type":"electronic","value":"9783642308857"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30885-7_10","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:50:45Z","timestamp":1340787045000},"page":"136-149","source":"Crossref","is-referenced-by-count":5,"title":["Toward a More Complete Alloy"],"prefix":"10.1007","author":[{"given":"Timothy","family":"Nelson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel J.","family":"Dougherty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kathi","family":"Fisler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shriram","family":"Krishnamurthi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"10_CR1","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.jsc.2009.03.003","volume":"45","author":"A. Abadi","year":"2010","unstructured":"Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. Journal of Symbolic Computation\u00a045(2), 153\u2013172 (2010)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BF01459101","volume":"99","author":"P. Bernays","year":"1928","unstructured":"Bernays, P., Sch\u00f6nfinkel, M.: Zum entscheidungsproblem der mathematischen Logik. Mathematische Annalen\u00a099, 342\u2013372 (1928)","journal-title":"Mathematische Annalen"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer (1997)","DOI":"10.1007\/978-3-642-59207-2"},{"key":"10_CR4","unstructured":"Chang, C.C., Keisler, J.: Model Theory, 3rd edn. Studies in Logic and the Foundations of Mathematics, vol.\u00a073. North-Holland (1990)"},{"key":"10_CR5","unstructured":"Claessen, K., Sorensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop on Model Computation (2003)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-36577-X_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2003","unstructured":"Fontaine, P., Gribomont, E.P.: Decidability of Invariant Validation for Paramaterized Systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 97\u2013112. Springer, Heidelberg (2003)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"issue":"2","key":"10_CR8","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J.A. Goguen","year":"1992","unstructured":"Goguen, J.A., Meseguer, J.: Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theor. Comput. Sci.\u00a0105(2), 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR9","unstructured":"Harrison, J.: Exploiting sorts in expansion-based proof procedures (unpublished manuscript), \n                    \n                      http:\/\/www.cl.cam.ac.uk\/~jrh13\/papers\/manysorted.pdf"},{"issue":"4","key":"10_CR10","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1015854101244","volume":"28","author":"J. Hooker","year":"2002","unstructured":"Hooker, J., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first-order logic. J. Automated Reasoning\u00a028(4), 371\u2013396 (2002)","journal-title":"J. Automated Reasoning"},{"key":"10_CR11","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0167-9236(88)90128-5","volume":"4","author":"R.G. Jereslow","year":"1988","unstructured":"Jereslow, R.G.: Computation-oriented reductions of predicate to propositional logic. Decision Support Systems\u00a04, 183\u2013197 (1988)","journal-title":"Decision Support Systems"},{"issue":"4","key":"10_CR12","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/s10990-007-9008-y","volume":"20","author":"S. Krishnamurthi","year":"2007","unstructured":"Krishnamurthi, S., Hopkins, P., McCarthy, J., Graunke, P., Pettyjohn, G., Felleisen, M.: Implementation and use of the PLT Scheme web server. Higher-Order and Symbolic Computation\u00a020(4), 431\u2013460 (2007)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-27813-9_40","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Seshia, S.A.: The UCLID Decision Procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 475\u2013478. Springer, Heidelberg (2004)"},{"issue":"3","key":"10_CR14","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H. Lewis","year":"1980","unstructured":"Lewis, H.: Complexity results for classes of quantificational formulas. J. Comp. and Sys. Sci.\u00a021(3), 317\u2013353 (1980)","journal-title":"J. Comp. and Sys. Sci."},{"issue":"6","key":"10_CR15","first-page":"37","volume":"128","author":"L. Momtahan","year":"2005","unstructured":"Momtahan, L.: Towards a small model theorem for data independent systems in Alloy. ENTCS\u00a0128(6), 37\u201352 (2005)","journal-title":"ENTCS"},{"key":"10_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-540-71070-7_35","volume-title":"Automated Reasoning","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 410\u2013425. Springer, Heidelberg (2008)"},{"key":"10_CR17","unstructured":"Nelson, T., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: On the finite model property in order-sorted logic. Tech. rep., Worcester Polytechnic Institute (2010), \n                    \n                      http:\/\/tinyurl.com\/osepl-tr-pdf"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-52337-6_16","volume-title":"Sorts and Types in Artificial Intelligence","author":"A. Oberschelp","year":"1990","unstructured":"Oberschelp, A.: Order Sorted Predicate Logic. In: Bl\u00e4sius, K.H., Rollinger, C.-R., Hedtst\u00fcck, U. (eds.) Sorts and Types in Artificial Intelligence. LNCS, vol.\u00a0418, pp. 1\u201317. Springer, Heidelberg (1990)"},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"30","author":"F.P. Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem in formal logic. Proceedings of the London Mathematical Society\u00a030, 264\u2013286 (1930)","journal-title":"Proceedings of the London Mathematical Society"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30885-7_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:33:07Z","timestamp":1620127987000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30885-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642308840","9783642308857"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30885-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}