Project OAF (Open Archive of Formalizations): Selected Publications

Please respect any copyrights when downloading
  1. Archival Literature
    1. Articles in Journals
    2. Papers at International, Peer-Reviewed Conferences
    3. Conference Proceedings Edited
  2. Theses
  3. Gray Literature
    1. Papers at Peer-Reviewed Workshops
  4. Unpublished

Archival Literature

Articles in Journals

  1. [1] J. Carette, W. M. Farmer, M. Kohlhase, and F. Rabe (2019) Big math and the one-brain barrier – a position paper and architecture proposal. Mathematical Intelligencer. Note: in press External Links: Link Cited by: p1.
  2. [2] G. Dowek, C. Dubois, B. Pientka, and F. Rabe (2017) Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Reports by Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik 6 (10), pp. 75–98. Note: see http://drops.dagstuhl.de/opus/volltexte/2017/6951/ Cited by: p1.
  3. [6] F. Rabe (2017) How to Identify, Translate, and Combine Logics?. Journal of Logic and Computation 27 (6), pp. 1753–1798. Cited by: p1.
  4. [7] F. Rabe (2017) Morphism Axioms. Theoretical Computer Science 691, pp. 55–80. Cited by: p1.
  5. [3] M. Kohlhase and F. Rabe (2016) QED reloaded: towards a pluralistic formal library of mathematical knowledge. Journal of Formalized Reasoning 9 (1), pp. 201–234. External Links: Link Cited by: p1.
  6. [4] F. Rabe (2015) Lax Theory Morphisms. ACM Transactions on Computational Logic 17 (1). Cited by: p1.
  7. [5] F. Rabe (2015) The Future of Logic: Foundation-Independence. Logica Universalis 10 (1), pp. 1–20. Note: 10.1007/s11787-015-0132-x; Winner of the Contest “The Future of Logic” at the World Congress on Universal Logic Cited by: p1.

Papers at International, Peer-Reviewed Conferences

  1. [8] D. Müller, F. Rabe, and C. Sacerdoti Coen (2019) The Coq Library as a Theory Graph. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2019, C. Kaliszyck, E. Brady, A. Kohlhase, and C. Sacerdoti Coen (Eds.), LNAI. Cited by: p1.
  2. [1] J. Betzendahl and M. Kohlhase (2018) Translating the IMPS theory library to OMDoc/MMT. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2018, F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.), LNAI. External Links: Link Cited by: p1.
  3. [6] D. Müller, M. Kohlhase, and F. Rabe (2018) Automatically finding theory morphisms for knowledge management. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2018, F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.), LNAI. External Links: Link Cited by: p1.
  4. [7] D. Müller, F. Rabe, and M. Kohlhase (2018) Theories as types. D. Galmiche, S. Schulz, and R. Sebastiani (Eds.), External Links: Link Cited by: p1.
  5. [4] M. Kohlhase, D. Müller, S. Owre, and F. Rabe (2017) Making PVS accessible to generic services by interpretation in a universal format. In Interactive theorem proving 8th international conference, itp 2017Interactive Theorem Proving, M. Ayala-Rincón and C. A. Muñoz (Eds.), LNCS, Vol. 10499. External Links: Link Cited by: p1.
  6. [5] D. Müller, T. Gauthier, C. Kaliszyk, M. Kohlhase, and F. Rabe (2017) Classification of alignments between concepts of formal mathematical systems. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2017, H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke (Eds.), LNAI. External Links: Link Cited by: p1.
  7. [2] M. Iancu, C. Jucovschi, M. Kohlhase, and T. Wiesing (2014) System description: MathHub.info. In Intelligent computer mathematicsIntelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, J. Urban, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCSLNCS, pp. 431–434. External Links: Link Cited by: p1.
  8. [3] C. Kaliszyk and F. Rabe (2014) Towards knowledge management for HOL Light. In Intelligent computer mathematicsIntelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, J. Urban, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCSLNCS, pp. 357–372. External Links: Link Cited by: p1.

Conference Proceedings Edited

  1. [2] F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.) (2018) Intelligent computer mathematics. LNAI, Springer. External Links: Document, ISBN 978-3-319-96811-7 Cited by: p1.
  2. [1] H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke (Eds.) (2017) Intelligent computer mathematics. LNAI, Springer. External Links: Document, ISBN 978-3-319-62074-9 Cited by: p1.

Theses

  1. [1] J. Betzendahl (2018-04) Translating the IMPS theory library to MMT / OMDoc. Master’s Thesis, Informatik, Universität Bielefeld. External Links: Link Cited by: p1.

Gray Literature

Papers at Peer-Reviewed Workshops

  1. [12] D. Müller, F. Rabe, and C. Sacerdoti Coen (2019) The Coq Library as a Theory Graph. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2019, C. Kaliszyck, E. Brady, A. Kohlhase, and C. Sacerdoti Coen (Eds.), LNAI. Cited by: p1.
  2. [13] D. Müller and F. Rabe (2019) Rapid prototyping formal systems in mmt: 5 case studies. In LFMTP 2019, External Links: Link Cited by: p1.
  3. [1] J. Betzendahl and M. Kohlhase (2018) Translating the IMPS theory library to OMDoc/MMT. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2018, F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.), LNAI. External Links: Link Cited by: p1.
  4. [10] D. Müller, M. Kohlhase, and F. Rabe (2018) Automatically finding theory morphisms for knowledge management. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2018, F. Rabe, W. M. Farmer, G. O. Passmore, and A. Youssef (Eds.), LNAI. External Links: Link Cited by: p1.
  5. [11] D. Müller, F. Rabe, and M. Kohlhase (2018) Theories as types. D. Galmiche, S. Schulz, and R. Sebastiani (Eds.), External Links: Link Cited by: p1.
  6. [15] F. Rabe and D. Müller (2018) Structuring theories with implicit morphisms. In 24th International Workshop on Algebraic Development Techniques 2018, External Links: Link Cited by: p1.
  7. [3] M. Codescu, T. Mossakowski, and F. Rabe (2017) Canonical Selection of Colimits. In Recent Trends in Algebraic Development Techniques, P. James and M. Roggenbach (Eds.), pp. 170–188. Cited by: p1.
  8. [14] D. Müller, C. Rothgang, Y. Liu, and F. Rabe (2017) Alignment-based translations across formal systems using interface theories. In Fifth Workshop on Proof eXchange for Theorem Proving - PxTP 2017, External Links: Link Cited by: p1.
  9. [21] F. Rabe (2017) The MMT Perspective on Conservativity. In Logical and Semantic Frameworks, with Applications, S. Alves and R. Wassermann (Eds.), pp. 17–33. Cited by: p1.
  10. [2] M. Codescu, T. Mossakowski, and F. Rabe (2016) Selecting Colimits for Parameterisation and Networks of Specifications. In Workshop on Algebraic Development Techniques, M. Roggenbach and P. James (Eds.), Cited by: p1.
  11. [6] C. Kaliszyk, F. Rabe, and G. Sutcliffe (2016) TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. In Workshop on Practical Aspects of Automated Reasoning, P. Fontaine, S. Schulz, and J. Urban (Eds.), pp. 41–55. Cited by: p1.
  12. [7] C. Kaliszyk, M. Kohlhase, D. Müller, and F. Rabe (2016) A standard for aligning mathematical concepts. In Intelligent computer mathematics – work in progress papersIntelligent Computer Mathematics – Work in Progress Papers, M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. Tompa, and M. Suda (Eds.), External Links: Link Cited by: p1.
  13. [9] R. Kumar and F. Rabe (2016) Breakout session on A standard for system integration and proof interchange. In Dagstuhl Seminar on Universality of Proofs, G. Dowek, C. Dubois, B. Pientka, and F. Rabe (Eds.), pp. 94–94. Cited by: p1.
  14. [20] F. Rabe (2016) MMT: A UniFormal Approach to Knowledge Representation. In Dagstuhl Seminar on Universality of Proofs, G. Dowek, C. Dubois, B. Pientka, and F. Rabe (Eds.), pp. 88–88. Cited by: p1.
  15. [4] F. Horozal and F. Rabe (2015) Formal Logic Definitions for Interchange Languages. In Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (Eds.), pp. 171–186. Cited by: p1.
  16. [19] F. Rabe (2015) Generic Literals. In Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (Eds.), pp. 102–117. Cited by: p1.
  17. [5] M. Iancu, C. Jucovschi, M. Kohlhase, and T. Wiesing (2014) System description: MathHub.info. In Intelligent computer mathematicsIntelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, J. Urban, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCSLNCS, pp. 431–434. External Links: Link Cited by: p1.
  18. [8] C. Kaliszyk and F. Rabe (2014) Towards knowledge management for HOL Light. In Intelligent computer mathematicsIntelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, J. Urban, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCSLNCS, pp. 357–372. External Links: Link Cited by: p1.
  19. [16] F. Rabe (2014) A Logic-Independent IDE. In Workshop on user interfaces for theorem proversWorkshop on User Interfaces for Theorem Provers, C. Benzmüller and B. Woltzenlogel Paleo (Eds.), pp. 48–60. External Links: Link Cited by: p1.
  20. [17] F. Rabe (2014) A Logic-Independent IDE. In Workshop on User Interfaces for Theorem Provers, C. Benzmüller and B. Woltzenlogel Paleo (Eds.), pp. 48–60. External Links: Document Cited by: p1.
  21. [18] F. Rabe (2014) MMT Objects. In Workshops and Work in Progress at CICM 2014: OpenMath Workshop, M. England, J. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, W. Neuper, P. Quaresma, A. Sexton, P. Sojka, J. Urban, and S. Watt (Eds.), Cited by: p1.

Unpublished

  1. [1] F. Rabe and D. Müller (2018) Structuring theories with implicit morphisms. Extended Abstract. External Links: Link Cited by: p1.