{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:31:27Z","timestamp":1725489087644},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730835"},{"type":"electronic","value":"9783540730866"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73086-6_15","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T06:57:56Z","timestamp":1187074676000},"page":"161-175","source":"Crossref","is-referenced-by-count":14,"title":["A Framework for Interactive Proof"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Winterstein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/3-540-44755-5_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Asperti","year":"2001","unstructured":"Asperti, A., Padovani, L., Coen, C.S., Schena, I.: HELM and the semantic math-web. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 59\u201374. Springer, Heidelberg (2001)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof General: A generic tool for proof development. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 38\u201342. Springer, Heidelberg (2000)"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Aspinall, D., L\u00fcth, C.: Proof General meets IsaWin. In: Aspinall, D., L\u00fcth,C. (eds.) User Interfaces for Theorem Provers UITP 2003, Electronic Notes in Theoretical Computer Science, vol. 103 (2003)","DOI":"10.1016\/j.entcs.2004.09.011"},{"key":"15_CR4","unstructured":"Aspinall, D., L\u00fcth, C.: Commentary on PGIP (2003-7), available from http:\/\/proofgeneral.inf.ed.ac.uk\/kit\/"},{"key":"15_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11618027_5","volume-title":"Mathematical Knowledge Management","author":"D. Aspinall","year":"2006","unstructured":"Aspinall, D., L\u00fcth, C., Wolff, B.: Assisted proof document authoring. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 65\u201380. Springer, Heidelberg (2006)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Cairns, P., Gow, J.: Integrating searching and authoring in Mizar. Journal of Automated Reasoning (to appear)","DOI":"10.1007\/s10817-007-9073-2"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s100090200076","volume":"4","author":"L.A. Dennis","year":"2003","unstructured":"Dennis, L.A., Collins, G., Norrish, M., Boulton, R.J., Slind, K., Melham, T.F.: The Prosper toolkit. International Journal on Software Tools for Technology Transfer\u00a04(2), 189\u2013210 (2003)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-540-30142-4_7","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Dixon","year":"2004","unstructured":"Dixon, L., Fleuriot, J.D.: Higher order rippling in IsaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 83\u201398. Springer, Heidelberg (2004)"},{"key":"15_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","DOI":"10.1007\/11826095","volume-title":"OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]","author":"M. Kohlhase","year":"2006","unstructured":"Kohlhase, M.: OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]. LNCS (LNAI), vol.\u00a04180. Springer, Heidelberg (2006)"},{"issue":"2","key":"15_CR10","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1017\/S0956796899003421","volume":"9","author":"C. L\u00fcth","year":"1999","unstructured":"L\u00fcth, C., Wolff, B.: Functional design and implementation of graphical user interfaces for theorem provers. Journal of Functional Programming\u00a09(2), 167\u2013189 (1999)","journal-title":"Journal of Functional Programming"},{"key":"15_CR11","unstructured":"Marc Wagner, C.B., Autexier, S.: PLATO: A mediator between text-editors and proof assistance systems. In: Benzm\u00fcller, C., Autexier, S. (eds.) 7th Workshop on User Interfaces for Theorem Provers (UITP 2006) (August 2006)"},{"key":"15_CR12","unstructured":"Mathweb homepage, http:\/\/www.mathweb.org\/"},{"key":"15_CR13","unstructured":"Mercer, A., Bundy, A., Duncan, H., Aspinall, D.: PG Tips, a recommender system for an interactive prover. Presented at MathUI workshop (2006)"},{"key":"15_CR14","unstructured":"MONET \u2014 mathematics on the web, Home page at http:\/\/monet.nag.co.uk\/"},{"key":"15_CR15","unstructured":"MoWGLI. mathematics on the web: Get it right by logics and interfaces, http:\/\/www.mowgli.cs.unibo.it\/"},{"key":"15_CR16","unstructured":"Proof General Kit home page, http:\/\/proofgeneral.inf.ed.ac.uk\/kit\/"},{"key":"15_CR17","unstructured":"RELAX NG XML schema language (2003), Home page at http:\/\/www.relaxng.org\/"},{"key":"15_CR18","unstructured":"Schreiner, W., Caprotti, O., Baraka, R.: The MathBroker project Johannes-Kepler-Universit\u00e4t Linz (2002), http:\/\/www.risc.uni-linz.ac.at\/projects\/basic\/mathbroker\/"},{"issue":"9","key":"15_CR19","doi-asserted-by":"publisher","first-page":"1381","DOI":"10.1109\/TCAD.2005.850814","volume":"24","author":"C.-J.H. Seger","year":"2005","unstructured":"Seger, C.-J.H., Jones, R.B., O\u2019Leary, J.W., Melham, T., Aagaard, M.D., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a024(9), 1381\u20131405 (2005)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"15_CR20","volume-title":"The Java Developer\u2019s Guide to Eclipse","author":"S. Shavor","year":"2003","unstructured":"Shavor, S., D\u2019Anjou, J., Fairborther, S., Kehn, D., Kellerman, J., McCarthy, P.: The Java Developer\u2019s Guide to Eclipse. Addison-Wesley, New York (2003)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Siekmann, J., Benzm\u00fcller, C., Autexier, S.: Computer supported mathematics with OMEGA. Journal of Applied Logic, special issue on Mathematics Assistance Systems\u00a04(4) (December 2006)","DOI":"10.1016\/j.jal.2005.10.008"},{"key":"15_CR22","unstructured":"The Eclipse Foundation. Project web site, http:\/\/www.eclipse.org"},{"key":"15_CR23","unstructured":"Timiriassova, E.: Tracking and visualizing dependency information within theories. Master\u2019s thesis, School of Informatics, University of Edinburgh (2005)"},{"key":"15_CR24","unstructured":"Trybulec, A., et al.: The Mizar project University of Bialystok, Poland (1973), http:\/\/mizar.org"},{"key":"15_CR25","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1145\/317636.317794","volume-title":"ICFP 1999","author":"M. Wallace","year":"1999","unstructured":"Wallace, M., Runciman, C.: Haskell and XML: Generic combinators or type-based translation? In: ICFP 1999. International Conference on Functional Programming, pp. 148\u2013159. ACM Press, New York (1999)"},{"key":"15_CR26","unstructured":"Wiedijk, F.: Digital math: systems implementing mathematics in the computer, http:\/\/www.cs.ru.nl\/~freek\/digimath\/"},{"key":"15_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/11814771_12","volume-title":"Automated Reasoning","author":"J. Zimmer","year":"2006","unstructured":"Zimmer, J., Autexier, S.: The MathServe system for semantic web reasoning services. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 140\u2013144. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Towards Mechanized Mathematical Assistants"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73086-6_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:59:43Z","timestamp":1619503183000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730835","9783540730866"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}