{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:22:57Z","timestamp":1742912577977,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_21","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"319-335","source":"Crossref","is-referenced-by-count":6,"title":["Making PVS Accessible to Generic Services by\u00a0Interpretation in a Universal Format"],"prefix":"10.1007","author":[{"given":"Michael","family":"Kohlhase","sequence":"first","affiliation":[]},{"given":"Dennis","family":"M\u00fcller","sequence":"additional","affiliation":[]},{"given":"Sam","family":"Owre","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The \n$$\\lambda \\Pi $$\n-calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp. 28\u201343 (2012)"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-08434-3_20","volume-title":"Intelligent Computer Mathematics","author":"T Gauthier","year":"2014","unstructured":"Gauthier, T., Kaliszyk, C.: Matching concepts across HOL libraries. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 267\u2013281. Springer, Cham (2014). doi:10.1007\/978-3-319-08434-3_20"},{"key":"21_CR3","unstructured":"MathHub PVS Git Repository. http:\/\/gl.mathhub.info\/PVS. Accessed 11 Apr 2017"},{"issue":"1","key":"21_CR4","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143\u2013184 (1993)","journal-title":"J. Assoc. Comput. Mach."},{"key":"21_CR5","doi-asserted-by":"publisher","unstructured":"Iancu, M., et al.: The Mizar mathematical library in OMDoc: translation and applications. J. Automated Reason. 50(2), 191\u2013202 (2013). doi:10.1007\/s10817-012-9271-4","DOI":"10.1007\/s10817-012-9271-4"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/978-3-319-08434-3_33","volume-title":"Intelligent Computer Mathematics","author":"M Iancu","year":"2014","unstructured":"Iancu, M., Jucovschi, C., Kohlhase, M., Wiesing, T.: System description: MathHub.info. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 431\u2013434. Springer, Cham (2014). doi:10.1007\/978-3-319-08434-3_33. http:\/\/kwarc.info\/kohlhase\/papers\/cicm14-mathhub.pdf. ISBN 978-3-319-08433-6"},{"key":"21_CR7","unstructured":"Iancu, M.: Towards flexiformal mathematics. Ph.D. thesis. Jacobs University, Bremen (2017)"},{"key":"21_CR8","unstructured":"Kaliszyk, C., et al.: A standard for aligning mathematical concepts. In: Kohlhase, M. et al. (eds.) Intelligent Computer Mathematics \u2013 Work in Progress Papers (2016). http:\/\/kwarc.info\/kohlhase\/papers\/cicmwip16-alignments.pdf"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Kohlhase, M.: OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2). Lecture Notes in Artificial Intelligence, vol. 4180. Springer, Heidelberg (2006)","DOI":"10.1007\/11826095"},{"key":"21_CR10","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Rabe, F.: Towards knowledge management for HOL light. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 357\u2013372. Springer, Cham (2014). doi:10.1007\/978-3-319-08434-3_26. http:\/\/kwarc.info\/frabe\/Research\/KR_hollight_14.pdf. ISBN 978-3-319-08433-6","DOI":"10.1007\/978-3-319-08434-3_26"},{"issue":"1","key":"21_CR11","first-page":"201","volume":"9","author":"M Kohlhase","year":"2016","unstructured":"Kohlhase, M., Rabe, F.: QED reloaded: towards a pluralistic formal library of mathematical knowledge. J. Formalized Reason. 9(1), 201\u2013234 (2016)","journal-title":"J. Formalized Reason."},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-642-14052-5_23","volume-title":"Interactive Theorem Proving","author":"A Krauss","year":"2010","unstructured":"Krauss, A., Schropp, A.: A mechanized translation from higher-order logic to set theory. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 323\u2013338. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14052-5_23"},{"issue":"1","key":"21_CR13","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-14052-5_22","volume-title":"Interactive Theorem Proving","author":"C Keller","year":"2010","unstructured":"Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307\u2013322. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14052-5_22"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/11856290_21","volume-title":"Artificial Intelligence and Symbolic Computation","author":"M Kohlhase","year":"2006","unstructured":"Kohlhase, M., Sucan, I.: A search engine for mathematical formulae. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS, vol. 4120, pp. 241\u2013253. Springer, Heidelberg (2006). doi:10.1007\/11856290_21"},{"key":"21_CR16","unstructured":"NASA Langley. Hypatheon: A Database Capability for PVS Theories (2016). https:\/\/shemesh.larc.nasa.gov\/people\/bld\/hypatheon.html"},{"key":"21_CR17","unstructured":"NASA Langley. NASA PVS Library (2016). http:\/\/shemesh.larc.nasa.gov\/fm\/ftp\/larc\/PVS-library\/pvslib.html"},{"key":"21_CR18","unstructured":"MathHub.info: Active Mathematics. http:\/\/mathhub.info. Accessed 28 Jan 2014"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/3-540-16492-8_94","volume-title":"Third International Conference on Logic Programming","author":"DA Miller","year":"1986","unstructured":"Miller, D.A., Nadathur, G.: Higher-order logic programming. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol. 225, pp. 448\u2013462. Springer, Heidelberg (1986). doi:10.1007\/3-540-16492-8_94"},{"issue":"1","key":"21_CR20","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J Meng","year":"2008","unstructured":"Meng, J., Paulson, L.: Translating higher-order clauses to first-order clauses. J. Automated Reason. 40(1), 35\u201360 (2008)","journal-title":"J. Automated Reason."},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). doi:10.1007\/3-540-55602-8_217"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/11814771_27","volume-title":"Automated Reasoning","author":"S Obua","year":"2006","unstructured":"Obua, S., Skalberg, S.: Importing HOL into Isabelle\/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 298\u2013302. Springer, Heidelberg (2006). doi:10.1007\/11814771_27"},{"key":"21_CR23","unstructured":"Pfenning, F., et al.: The Logosphere Project (2003). http:\/\/www.logosphere.org\/"},{"key":"21_CR24","unstructured":"The PVS libraries in OMDoc\/MMT format. https:\/\/gl.mathhub.info\/PVS. Accessed 29 May 2017"},{"key":"21_CR25","unstructured":"Rabe, F.: A logic-independent IDE. In: Benzm\u00fcller, C., Woltzenlogel Paleo, B. (eds.) Workshop on User Interfaces for Theorem Provers, pp. 48\u201360 (2014). Elsevier"},{"key":"21_CR26","doi-asserted-by":"publisher","unstructured":"Rabe, F.: How to identify, translate, and combine logics? J. Logic Comput. (2014). doi:10.1093\/logcom\/exu079","DOI":"10.1093\/logcom\/exu079"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-20615-8_7","volume-title":"Intelligent Computer Mathematics","author":"F Rabe","year":"2015","unstructured":"Rabe, F.: Generic literals. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 102\u2013117. Springer, Cham (2015). doi:10.1007\/978-3-319-20615-8_7"},{"key":"21_CR28","unstructured":"Rabe, F.: A Modular Type Reconstruction Algorithm (2017). http:\/\/kwarc.info\/frabe\/Research\/rabe_recon_17.pdf"},{"issue":"1","key":"21_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2013.06.001","volume":"230","author":"F Rabe","year":"2013","unstructured":"Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230(1), 1\u201354 (2013)","journal-title":"Inf. Comput."},{"key":"21_CR30","unstructured":"vis.js - A dynamic, browser based visualization library. http:\/\/visjs.org. Accessed 04 May 2017"},{"key":"21_CR31","doi-asserted-by":"publisher","unstructured":"Watt, S.M., et al. (eds.) Intelligent Computer Mathematics. LNCS, vol. 8543. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-08434-3. ISBN 978-3-319-08433-6","DOI":"10.1007\/978-3-319-08434-3"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:07:09Z","timestamp":1664431629000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}