{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:26:02Z","timestamp":1725492362085},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540755586"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75560-9_4","type":"book-chapter","created":{"date-parts":[[2007,10,6]],"date-time":"2007-10-06T05:36:46Z","timestamp":1191649006000},"page":"17-31","source":"Crossref","is-referenced-by-count":6,"title":["Decidable Fragments of Many-Sorted Logic"],"prefix":"10.1007","author":[{"given":"Aharon","family":"Abadi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Rabinovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"The alloy analyzer home page, http:\/\/alloy.mit.edu"},{"key":"4_CR2","unstructured":"http:\/\/alloy.mit.edu\/case-studies.php"},{"key":"4_CR3","unstructured":"Abadi, A.: Decidable fragments of many-sorted logic. Master\u2019s thesis, Tel-Aviv University (2007)"},{"key":"4_CR4","unstructured":"Beauquier, D., Slissenko, A.: Verification of timed algorithms: Gurevich abstract state machines versus first order timed logic. In: Proc. of ASM 2000 International Workshop (March 2000)"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1016\/S0304-3975(01)00186-4","volume":"275","author":"D. Beauquier","year":"2002","unstructured":"Beauquier, D., Slissenko, A.: Decidable verification for reducible timed automata specified in a first order logic with time. Theoretical Computer Science\u00a0275, 347\u2013388 (2002)","journal-title":"Theoretical Computer Science"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/S0168-0072(01)00049-5","volume":"113","author":"D. Beauquier","year":"2002","unstructured":"Beauquier, D., Slissenko, A.: A first order logic for specification of timed algorithms: Basic properties and a decidable class. Annals of Pure and Applied Logic\u00a0113, 13\u201352 (2002)","journal-title":"Annals of Pure and Applied Logic"},{"key":"4_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. Borger","year":"1997","unstructured":"Borger, E., Gradel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)"},{"issue":"1","key":"4_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"4_CR9","doi-asserted-by":"publisher","first-page":"1237","DOI":"10.2307\/2274274","volume":"49","author":"W.D. Goldfarb","year":"1984","unstructured":"Goldfarb, W.D.: The unsolvability of the godel class with identity. The Journal of Symbolic Logic\u00a049(4), 1237\u20131252 (1984)","journal-title":"The Journal of Symbolic Logic"},{"issue":"2","key":"4_CR10","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol.\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng . Methodol."},{"key":"4_CR11","unstructured":"Jackson, D.: Micromodels of software:lightweight modelling and analysis with alloy. Technical report, MIT Lab for Computer Science (2002)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: CADE, pp. 99\u2013115 (2005)","DOI":"10.1007\/11532231_8"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Mortimer, M.: On languages with two variables. Zeitschr. f. math. Logik u. Grundlagen d. Math., 135\u2013140 (1975)","DOI":"10.1002\/malq.19750210118"},{"issue":"2-3","key":"4_CR14","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"4_CR15","volume-title":"The Z notation: a reference manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z notation: a reference manual. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"4_CR16","first-page":"141","volume-title":"CADE-13","author":"C. Weidenbach","year":"1996","unstructured":"Weidenbach, C., Gaede, B., Rock, G.: Spass & flotter version 0.42. In: CADE-13. Proceedings of the 13th International Conference on Automated Deduction, pp. 141\u2013145. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75560-9_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:24:48Z","timestamp":1619519088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75560-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755586"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75560-9_4","relation":{},"subject":[]}}