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 (2021) Big math and the one-brain barrier – the tetrapod model of mathematical knowledge. Mathematical Intelligencer 43 (1). External Links: Document Cited by: p1.
  2. [4] M. Kohlhase and F. Rabe (2021) Experiences from exporting major proof assistant libraries. Journal of Automated Reasoning 65 (8), pp. 1265–1298. External Links: Document Cited by: p1.
  3. [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.
  4. [7] F. Rabe (2017) How to Identify, Translate, and Combine Logics?. Journal of Logic and Computation 27 (6), pp. 1753–1798. Cited by: p1.
  5. [8] F. Rabe (2017) Morphism Axioms. Theoretical Computer Science 691, pp. 55–80. Cited by: p1.
  6. [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.
  7. [5] F. Rabe (2015) Lax Theory Morphisms. ACM Transactions on Computational Logic 17 (1). Cited by: p1.
  8. [6] F. Rabe (2015) The Future of Logic: Foundation-Independence. Logica Universalis 10 (1), pp. 1–20. Note: Winner of the Contest “The Future of Logic” at the World Congress on Universal Logic External Links: Document, Link Cited by: p1.

Papers at International, Peer-Reviewed Conferences

  1. [5] M. Kohlhase, F. Rabe, C. S. Coen, and J. F. Schaefer (2020) Logic-independent proof search in logical frameworks (short paper). In 10th international joint conference on automated reasoning (IJCAR 2020)10th International Joint Conference on Automated Reasoning (IJCAR 2020), N. Peltier and V. Sofronie-Stokkermans (Eds.), pp. 395–401. Cited by: p1.
  2. [9] D. Müller, F. Rabe, C. Rothgang, and M. Kohlhase (2020) Representing structural language features in formal meta-languages. In Intelligent computer mathematicsIntelligent Computer Mathematics (CICM) 2020, C. Benzmüller and B. Miller (Eds.), LNAI, Vol. 12236, pp. 206–221. External Links: Link Cited by: p1.
  3. [10] 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.
  4. [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.
  5. [7] 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.
  6. [8] D. Müller, F. Rabe, and M. Kohlhase (2018) Theories as types. In 9th international joint conference on automated reasoning9th International Joint Conference on Automated Reasoning, D. Galmiche, S. Schulz, and R. Sebastiani (Eds.), External Links: Link Cited by: p1.
  7. [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.
  8. [6] 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.
  9. [2] M. Iancu, C. Jucovschi, M. Kohlhase, and T. Wiesing (2014) System description: MathHub.info. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 431–434. External Links: Link Cited by: p1.
  10. [3] C. Kaliszyk and F. Rabe (2014) Towards knowledge management for HOL Light. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, 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. [2] D. Müller (2019-12) Mathematical knowledge management across formal libraries. Ph.D. Thesis, Informatics, FAU Erlangen-Nürnberg. External Links: Link Cited by: p1.
  2. [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. [14] F. Rabe and N. Roux (2021) Systematic translation of formalizations of type theory from intrinsic to extrinsic style. In Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), E. Pimentel and E. Tassi (Eds.), External Links: Link, Document Cited by: p1.
  2. [15] F. Rabe and N. Roux (2021) Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style. In Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), E. Pimentel and E. Tassi (Eds.), pp. 88–103. Cited by: p1.
  3. [22] N. Roux and F. Rabe (2021) Structure-Preserving Diagram Operators. In Recent Trends in Algebraic Development Techniques, M. Roggenbach (Ed.), Lecture Notes in Computer Science, Vol. 12669, pp. 142–163. External Links: Link, ISBN 978-3-030-73785-6, Document Cited by: p1.
  4. [8] M. Kohlhase, F. Rabe, and M. Wenzel (2020) Making Isabelle content accessible in knowledge representation formats. In Proceedings of the 25th International Conference on Types for Proofs and Programs, TYPES 2019, M. Bezem and A. Mahboubi (Eds.), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 175. External Links: ISBN 978-3-95977-158-0, Link, Document Cited by: p1.
  5. [11] 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.
  6. [10] D. Müller, F. Rabe, and M. Kohlhase (2018) Theories as types. In 9th international joint conference on automated reasoning9th International Joint Conference on Automated Reasoning, D. Galmiche, S. Schulz, and R. Sebastiani (Eds.), External Links: Link Cited by: p1.
  7. [13] 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.
  8. [2] 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.
  9. [12] 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.
  10. [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.
  11. [1] 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.
  12. [5] 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.
  13. [6] 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.
  14. [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.
  15. [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.
  16. [3] 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.
  17. [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.
  18. [4] M. Iancu, C. Jucovschi, M. Kohlhase, and T. Wiesing (2014) System description: MathHub.info. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 431–434. External Links: Link Cited by: p1.
  19. [7] C. Kaliszyk and F. Rabe (2014) Towards knowledge management for HOL Light. In Intelligent computer mathematicsIntelligent Computer Mathematics 2014, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban (Eds.), LNCS, pp. 357–372. External Links: Link Cited by: p1.
  20. [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.
  21. [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.
  22. [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. [10] N. Roux (2021-03-22) A beginner’s guide to logical relations for a logical framework. seminar paper, FAU Erlangen-Nürnberg. Note: written as a student of the kwarc seminar External Links: Link Cited by: p1.
  2. [9] N. Roux (2021-01-27) A beginner’s guide to logical relations for a logical framework (slides). seminar presentation, FAU Erlangen-Nürnberg. Note: presented as a student of the kwarc seminar External Links: Link Cited by: p1.
  3. [5] F. Rabe and N. Roux (2021) Modular formalization of formal systems. Note: under review External Links: Link Cited by: p1.
  4. [8] N. Roux and F. Rabe (2021) Structure-Preserving Diagram Operators. In Recent Trends in Algebraic Development Techniques, M. Roggenbach (Ed.), Lecture Notes in Computer Science, Vol. 12669, pp. 142–163. External Links: Link, ISBN 978-3-030-73785-6, Document Cited by: 7.
  5. [1] M. Kohlhase, F. Rabe, C. S. Coen, and J. F. Schaefer (2020) Logic-independent proof search in logical frameworks (extended report). Note: extended report of conference submission External Links: Link Cited by: p1.
  6. [2] M. Kohlhase, F. Rabe, and M. Wenzel (2020) Making Isabelle content accessible in knowledge representation formats. External Links: Link, 2005.08884 Cited by: p1.
  7. [3] M. Kohlhase and F. Rabe (2020) Experiences from exporting major proof assistant libraries. External Links: Link, 2005.03089 Cited by: p1.
  8. [6] N. Roux and F. Rabe (2020) Diagram Operators in a Logical Framework. Extended Abstract, Frontiers in Artificial Intelligence and Applications. External Links: Link Cited by: p1.
  9. [7] N. Roux and F. Rabe (2020) Functorial Diagram Operators. Extended Abstract. Note: Extended abstract accepted as [8] Cited by: p1.
  10. [4] F. Rabe and D. Müller (2018) Structuring theories with implicit morphisms. Extended Abstract. External Links: Link Cited by: p1.