{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:32:14Z","timestamp":1742383934401},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672821"},{"type":"electronic","value":"9783540464198"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_7","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T23:17:25Z","timestamp":1186615045000},"page":"78-92","source":"Crossref","is-referenced-by-count":31,"title":["The PROSPER Toolkit"],"prefix":"10.1007","author":[{"given":"Louise A.","family":"Dennis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graham","family":"Collins","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Boulton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graham","family":"Robinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mike","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"Melham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"7_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-48256-3_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. D. Aagaard","year":"1999","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. Y. Bertot, G. Dowek, A. Hirshowitz, C. Paulin and L. Th\u00e9ry (eds), Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1690, Springer-Verlag, pp. 323\u2013340, 1999. 89"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, A. Meirer, E. Melis, W. Schaarschmidt, J. Siekmann, and V. Sorge, \u2126MEGA, Towards a mathematical assistant. 14th Conference on Automated Deduction, W. McCune (ed), Lecture Notes in Artificial Intelligence 1249, Springer-Verlag, pp. 252\u2013255, 1997. 89","DOI":"10.1007\/3-540-63104-6_23"},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BFb0055131","volume-title":"Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics","author":"R. Boulton","year":"1998","unstructured":"R. Boulton, K. Slind, A. Bundy, and M. Gordon, An interface between CLAM and HOL. J. Grundy and M. Newey (eds), Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1479, Springer-Verlag, pp. 87\u2013104, 1998. 89"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"B. Brock, M. Kaufmann, and J Moore, ACL2 Theorems about Commercial Microprocessors. M. Srivas and A. Camilleri (eds), Proceedings of Formal Methods in Computer-Aided Design (FMCAD\u201996), Springer-Verlag, pp. 275\u2013293, 1996. 83, 90","DOI":"10.1007\/BFb0031816"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, C. Horn, and A. Smaill, The Oyster-Clam system. 10th International Conference on Automated Deduction, M. E. Stickel (ed), Lecture Notes in Artificial Intelligence 449, Springer-Verlag, pp. 647\u2013648, 1990. 89","DOI":"10.1007\/3-540-52885-7_123"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church, A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic, vol. 5, pp. 56\u201368, 1940. 80, 82","journal-title":"The Journal of Symbolic Logic"},{"key":"7_CR7","first-page":"65","volume-title":"Extended abstract in Proceedings of the First Workshop on Abstraction, Analogy and Metareasoning","author":"A. Coglio","year":"1996","unstructured":"A. Coglio, The Control Component of OMRS: NQTHM as a Case Study. Extended abstract in Proceedings of the First Workshop on Abstraction, Analogy and Metareasoning, IRST, Trento, Italy, pp. 65\u201371, 1996. 90"},{"key":"7_CR8","unstructured":"J. Fitzgerald and P. G. Larsen, Modelling Systems: Practical Tools and Techniques in Software Development, Cambridge University Press, 1998. 80"},{"issue":"3","key":"7_CR9","first-page":"156","volume":"5","author":"A. Franke","year":"1999","unstructured":"A. Franke, S. M. Hess, C. G. Jung, M. Kohlhase, and V. Sorge, Agent-Oriented Integration of Distributed Mathematical Services. Journal of Universal Computer Science, 5(3), pp. 156\u2013187, 1999. 89","journal-title":"Journal of Universal Computer Science"},{"key":"7_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-59293-8_187","volume-title":"Proceedings TAPSOFT\u201995","author":"J. A. Goguen","year":"1995","unstructured":"J. A. Goguen and Luqi, Formal methods and social context in software development. Proceedings TAPSOFT\u201995, Lecture Notes in Computer Science 915. Springer-Verlag, pp. 62\u201381, 1995. 78"},{"key":"7_CR11","unstructured":"M. J. C. Gordon and T. F. Melham (eds), Introduction to HOL: A theorem proving environment for higher order logic, Cambridge University Press, 1993. 79"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia, P. Pecchiari, and C. Talcott, Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. F. Baader and K. U. Schulz (eds), Frontiers of Combining Systems-First International Workshop (FroCoS\u201996), Kluwer\u2019s Applied Logic Series (APLS), pp. 157\u2013174, 1996. 90","DOI":"10.1007\/978-94-009-0349-4_8"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"A. Holt and E. Klein, A semantically-derived subset of English for hardware verification. 37th Annual Meeting of the Association for Computational Linguistics: Proceedings of the Conference, Association for Computational Linguistics, pp. 451\u2013456, 1999. 85","DOI":"10.3115\/1034678.1034747"},{"key":"7_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"J. Hurd, Integrating Gandalf and HOL. Y. Bertot, G. Dowek, A. Hirshowitz, C. Paulin and L. Th\u00e9ry (eds). Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1690, Springer-Verlag, pp. 311\u2013321, 1999. 83"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"J. Joyce and C.-J. Seger, Linking BDD based symbolic evaluation to interactive theorem proving. ACM\/IEEE Design Automation Conference, June 1993. 89","DOI":"10.1145\/157485.164981"},{"key":"7_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1186","DOI":"10.1007\/3-540-48118-4_13","volume-title":"FM\u201999-Formal Methods","author":"B. Kreig-Br\u00fckner","year":"1999","unstructured":"B. Kreig-Br\u00fckner, J. Peleska, E.-R. Olderog, and A. Baer, The UniForM Work-Bench, a Universal Development Environment for Formal Methods. J. M. Wing, J. Woodcock and J. Davies (eds), FM\u201999-Formal Methods, vol. 2, Lecture Notes in Computer Science 1709, pp. 1186\u20131205, 1999. 90"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers. 1993. 83","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"7_CR18","unstructured":"Microsoft Corporation, Microsoft Excel, http:\/\/www.microsoft.com\/excel . 87"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"R. Milner, M. Tofte, R. Harper and D. MacQueen, The Definition of Standard ML (Revised), MIT Press, 1997. 80","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"7_CR20","unstructured":"J. O\u2019Leary, X. Zhao, R. Gerth, and C.-J. H. Seger, Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, First Quarter, 1999. Online at http:\/\/developer.intel.com\/technology\/itj\/ . 89"},{"key":"7_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"International Conference on Computer-Aided Verification","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M. Srivas, An integration of model checking and automatedpro of checking. International Conference on Computer-Aided Verification, Lecture Notes in Computer Science 939, Springer-Verlag, pp. 84\u201397, 1995. 89"},{"key":"7_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","volume-title":"The Second International Conference on Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"1998","unstructured":"M. Sheeran and G. St\u00e5lmarck, A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. The Second International Conference on Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 1522, Springer-Verlag, pp. 82\u201399, 1998. 83, 88"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"G. St\u00e5lmarck and M. S\u00e4flund, Modelling and Verifying Systems and Software in Propositional Logic. Proceedings of SAFECOMP\u2019 90, Pergamon Press, pp. 31\u201336, 1990. 83, 88","DOI":"10.1016\/B978-0-08-040953-5.50011-8"},{"issue":"1 + 2","key":"7_CR24","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/s100090050003","volume":"1","author":"B. Steffen","year":"1997","unstructured":"B. Steffen, T. Margaria, and V. Braun, The Electronic Tool Integration Platform: concepts and design. International Journal on Software Tools for Technology Transfer, 1(1 + 2), pp. 9\u201330, 1997. 89","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"7_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-61511-3_65","volume-title":"13th International Conference on Automated Deduction","author":"T. Tammet","year":"1996","unstructured":"T. Tammet, A resolution theorem prover for intuitionistic logic. 13th International Conference on Automated Deduction, Lecture Notes in Computer Science 1104, Springer-Verlag, pp. 2\u201316, 1996. 83"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T21:07:24Z","timestamp":1556744844000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}