Document Open Access Logo

Making Isabelle Content Accessible in Knowledge Representation Formats

Authors Michael Kohlhase , Florian Rabe, Makarius Wenzel

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2019.1.pdf
  • Filesize: 0.83 MB
  • 24 pages

Document Identifiers

Author Details

Michael Kohlhase
  • University Erlangen-Nürnberg, Germany
Florian Rabe
  • University Erlangen-Nürnberg, Germany
Makarius Wenzel
  • Selfemployed, Augsburg, Germany

Funding

The authors were supported by DFG grant RA-18723-1 OAF and EU grant Horizon 2020 ERI 676541 OpenDreamKit.

Cite AsGet BibTex

Michael Kohlhase, Florian Rabe, and Makarius Wenzel. Making Isabelle Content Accessible in Knowledge Representation Formats. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.TYPES.2019.1

Abstract

The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved too difficult. After substantial improvements of the Isabelle Prover IDE (PIDE) and the OMDoc/Mmt format since then, we are now able to deliver such an export. Concretely we present an integration of PIDE and Mmt that allows exporting all Isabelle libraries in OMDoc format. Our export covers the full Isabelle distribution and the Archive of Formal Proofs (AFP) - more than 12 thousand theories and locales resulting in over 65 GB of OMDoc/XML. Such a systematic export of Isabelle content to a well-defined interchange format like OMDoc enables many applications such as dependency management, independent proof checking, or library search.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Isabelle
  • PIDE
  • OMDoc
  • MMT
  • library
  • export

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Archive of formal proofs (AFP), April 2020. URL: https://www.isa-afp.org.
  2. S. Autexier, D. Hutter, H. Mantel, and A. Schairer. Towards an Evolutionary Formal Software-Development Using CASL. In D. Bert, C. Choppy, and P. Mosses, editors, WADT, volume 1827 of Lecture Notes in Computer Science, pages 73-88. Springer, 1999. Google Scholar
  3. Clemens Ballarin. Locales: A module system for mathematical theories. JAR, 52(2):123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  4. H. Barendregt and H. Geuvers. Proof assistants using dependent type systems. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier, 2001. Google Scholar
  5. Katja Berčič, Michael Kohlhase, and Florian Rabe. Towards a heterogeneous query language for mathematical knowledge - extended report, 2020. URL: http://kwarc.info/kohlhase/papers/tetrasearch.pdf.
  6. J. Betzendahl and M. Kohlhase. Translating the imps theory library to mmt/omdoc. In F. Rabe, W. Farmer, G. Passmore, and A. Youssef, editors, Intelligent Computer Mathematics, volume 11006, pages 7-22. Springer, 2018. Google Scholar
  7. M. Boespflug, Q. Carbonneaux, and O. Hermant. The λΠ-calculus modulo as a universal proof language. In D. Pichardie and T. Weber, editors, Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pages 28-43, 2012. Google Scholar
  8. Timothy Bourke, Matthias Daum, Gerwin Klein, and Rafal Kolanski. Challenges and experiences in managing large-scale proofs. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Intelligent Computer Mathematics - 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings, volume 7362 of Lecture Notes in Computer Science, pages 32-48. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31374-5_3.
  9. A. Condoluci, M. Kohlhase, D. Müller, F. Rabe, C. Sacerdoti Coen, and M. Wenzel. Relational Data Across Mathematical Libraries. In C. Kaliszyk, E. Brady, A. Kohlhase, and C. Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 61-76. Springer, 2019. Google Scholar
  10. T. Gauthier and C. Kaliszyk. Matching concepts across HOL libraries. In S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban, editors, Intelligent Computer Mathematics, pages 267-281. Springer, 2014. Google Scholar
  11. M. J. C. Gordon. HOL: A machine oriented formulation of higher order logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985. Google Scholar
  12. M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of LNCS. Springer, 1979. Google Scholar
  13. F. Haftmann and M. Wenzel. Constructive Type Classes in Isabelle. In T. Altenkirch and C. McBride, editors, TYPES conference, pages 160-174. Springer, 2006. Google Scholar
  14. Florian Haftmann and Makarius Wenzel. Local theory specifications in Isabelle/Isar. In Stefano Berardi, Ferruccio Damiani, and Ugo de Liguoro, editors, Types for Proofs and Programs, TYPES 2008, volume 5497 of LNCS. Springer, 2009. Google Scholar
  15. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993. Google Scholar
  16. Fulya Horozal, Michael Kohlhase, and Florian Rabe. Extending MKM formats at the statement level. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Intelligent Computer Mathematics, number 7362 in LNAI, pages 65-80. Springer Verlag, 2012. URL: http://kwarc.info/kohlhase/papers/mkm12-p2s.pdf.
  17. Mihnea Iancu, Michael Kohlhase, Florian Rabe, and Josef Urban. The Mizar Mathematical Library in OMDoc: Translation and applications. Journal of Automated Reasoning, 50(2):191-202, 2013. URL: https://doi.org/10.1007/s10817-012-9271-4.
  18. Fabian Immler, Jonas Rädle, and Makarius Wenzel. Virtualization of HOL4 in Isabelle. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International conference on Interactive Theorem Proving (ITP 2019), volume 141 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: http://drops.dagstuhl.de/opus/volltexte/2019/11076/pdf/LIPIcs-ITP-2019-21.pdf.
  19. Isabelle website, April 2020. URL: https://isabelle.in.tum.de/website-Isabelle2020.
  20. Isabelle/MMT for Isabelle2020, April 2020. URL: https://files.sketis.net/Isabelle_MMT-20200421.
  21. C. Kaliszyk, M. Kohlhase, D. Müller, and F. Rabe. A Standard for Aligning Mathematical Concepts. In A. Kohlhase, M. Kohlhase, P. Libbrecht, B. Miller, F. Tompa, A. Naummowicz, W. Neuper, P. Quaresma, and M. Suda, editors, Work in Progress at CICM 2016, pages 229-244. CEUR-WS.org, 2016. Google Scholar
  22. C. Kaliszyk and J. Urban. HOL(y)hammer: Online ATP service for HOL light. Mathematics in Computer Science, 9(1):5-22, 2015. Google Scholar
  23. Cezary Kaliszyk and Alexander Krauss. Scalable LCF-style proof translation. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 51-66, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  24. Cezary Kaliszyk and Florian Rabe. Towards knowledge management for HOL Light. In Stephan Watt, James Davenport, Alan Sexton, Petr Sojka, and Josef Urban, editors, Intelligent Computer Mathematics 2014, number 8543 in LNCS, pages 357-372. Springer, 2014. URL: http://kwarc.info/frabe/Research/KR_hollight_14.pdf.
  25. F. Kammüller, M. Wenzel, and L. Paulson. Locales - a Sectioning Concept for Isabelle. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, pages 149-166. Springer, 1999. Google Scholar
  26. C. Keller and B. Werner. Importing HOL Light into Coq. In M. Kaufmann and L. Paulson, editors, Interactive Theorem Proving, pages 307-322. Springer, 2010. Google Scholar
  27. M. Kohlhase. OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2). Number 4180 in Lecture Notes in Artificial Intelligence. Springer, 2006. Google Scholar
  28. M. Kohlhase, D. Müller, S. Owre, and F. Rabe. Making PVS Accessible to Generic Services by Interpretation in a Universal Format. In M. Ayala-Rincon and C. Munoz, editors, Interactive Theorem Proving, pages 319-335. Springer, 2017. Google Scholar
  29. M. Kohlhase and F. Rabe. QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge. Journal of Formalized Reasoning, 9(1):201-234, 2016. Google Scholar
  30. M. Kohlhase and I. Şucan. A Search Engine for Mathematical Formulae. In T. Ida, J. Calmet, and D. Wang, editors, Artificial Intelligence and Symbolic Computation, pages 241-253. Springer, 2006. Google Scholar
  31. Michael Kohlhase. The flexiformalist manifesto. In Andrei Voronkov, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen M. Watt, and Daniela Zaharie, editors, 14th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012), pages 30-36, Timisoara, Romania, 2013. IEEE Press. URL: http://kwarc.info/kohlhase/papers/synasc13.pdf.
  32. Michael Kohlhase and Florian Rabe. Experiences from exporting major proof assistant libraries. submitted, 2020. URL: https://kwarc.info/people/frabe/Research/KR_oafexp_20.pdf.
  33. Michael Kohlhase and Ioan Şucan. A search engine for mathematical formulae. In Tetsuo Ida, Jacques Calmet, and Dongming Wang, editors, Proceedings of Artificial Intelligence and Symbolic Computation, AISC'2006, number 4120 in LNAI, pages 241-253. Springer Verlag, 2006. URL: http://kwarc.info/kohlhase/papers/aisc06.pdf.
  34. A. Krauss and A. Schropp. A Mechanized Translation from Higher-Order Logic to Set Theory. In M. Kaufmann and L. Paulson, editors, Interactive Theorem Proving, pages 323-338. Springer, 2010. Google Scholar
  35. J. Meng and L. Paulson. Translating Higher-Order Clauses to First-Order Clauses. Journal of Automated Reasoning, 40(1):35-60, 2008. Google Scholar
  36. D. Müller, M. Kohlhase, and F. Rabe. Automatically Finding Theory Morphisms for Knowledge Management. In F. Rabe, W. Farmer, G. Passmore, and A. Youssef, editors, Intelligent Computer Mathematics, pages 209-224. Springer, 2018. Google Scholar
  37. D. Müller and F. Rabe. Rapid Prototyping Formal Systems in MMT: Case Studies. In D. Miller and I. Scagnetto, editors, Logical Frameworks and Meta-languages: Theory and Practice, pages 40-54, 2019. Google Scholar
  38. D. Müller, F. Rabe, and C. Sacerdoti Coen. The Coq Library as a Theory Graph. In C. Kaliszyk, E. Brady, A. Kohlhase, and C. Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 171-186. Springer, 2019. Google Scholar
  39. Dennis Müller, Florian Rabe, Colin Rothgang, and Michael Kohlhase. Representing structural language features in formal meta-languages. submitted, 2020. URL: http://kwarc.info/kohlhase/submit/cicm20-features.pdf.
  40. T. Nipkow and C. Prehofer. Type checking type classes. In ACM Symp. Principles of Programming Languages, 1993. Google Scholar
  41. S. Obua and S. Skalberg. Importing HOL into Isabelle/HOL. In N. Shankar and U. Furbach, editors, Automated Reasoning, volume 4130. Springer, 2006. Google Scholar
  42. Karl Palmskog, Ahmet Çelik, and Milos Gligoric. piCoq: parallel regression proving for large-scale verification projects. In Frank Tip and Eric Bodden, editors, Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018, Amsterdam, The Netherlands, July 16-21, 2018, pages 344-355. ACM, 2018. URL: https://doi.org/10.1145/3213846.3213877.
  43. Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In Logic and Computer Science, pages 361-386. Academic Press, 1990. URL: http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz.
  44. Lawrence C. Paulson, Tobias Nipkow, and Makarius Wenzel. From LCF to Isabelle/HOL. Formal Aspects of Computing, September 2019. Springer, London. URL: https://doi.org/10.1007/s00165-019-00492-1.
  45. A. Pitts. The HOL logic. In M. J. C. Gordon and T. F. Melham, editors, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, pages 191-232. Cambridge University Press, 1993. Google Scholar
  46. F. Rabe. A Logic-Independent IDE. In C. Benzmüller and B. Woltzenlogel Paleo, editors, Workshop on User Interfaces for Theorem Provers, pages 48-60. Elsevier, 2014. Google Scholar
  47. F. Rabe. How to Identify, Translate, and Combine Logics? Journal of Logic and Computation, 27(6):1753-1798, 2017. Google Scholar
  48. F. Rabe and M. Kohlhase. A Scalable Module System. Information and Computation, 230(1):1-54, 2013. Google Scholar
  49. Makarius Wenzel. Asynchronous user interaction and tool integration in Isabelle/PIDE. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving (ITP 2014), volume 8558 of LNCS. Springer, 2014. Google Scholar
  50. Makarius Wenzel. Interaction with formal mathematical documents in Isabelle/PIDE. In Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics (CICM 2019), volume 11617 of LNAI. Springer, 2019. URL: http://arxiv.org/abs/1905.01735.
  51. Makarius Wenzel. The Isabelle/Isar Implementation, April 2020. URL: https://isabelle.in.tum.de/website-Isabelle2020/dist/doc/implementation.pdf.
  52. Makarius Wenzel. Isabelle/jEdit, April 2020. URL: https://isabelle.in.tum.de/website-Isabelle2020/dist/doc/jedit.pdf.
  53. Makarius Wenzel. The Isabelle System manual, April 2020. URL: https://isabelle.in.tum.de/website-Isabelle2020/dist/doc/system.pdf.
  54. Markus Wenzel. Isar - a generic interpretative approach to readable formal proof documents. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics: TPHOLs '99, volume 1690 of LNCS. Springer, 1999. Google Scholar
  55. Mark D. Wilkinson, Michel Dumontier, IJsbrand Jan Aalbersberg, Gabrielle Appleton, Myles Axton, Arie Baak, Niklas Blomberg, Jan-Willem Boiten, Luiz Bonino da Silva Santos, Philip E. Bourne, Jildau Bouwman, Anthony J. Brookes, Tim Clark, Mercè Crosas, Ingrid Dillo, Olivier Dumon, Scott Edmunds, Chris T. Evelo, Richard Finkers, Alejandra Gonzalez-Beltran, Alasdair J. G. Gray, Paul Groth, Carole Goble, Jeffrey S. Grethe, Jaap Heringa, Peter A. C 't Hoen, Rob Hooft, Tobias Kuhn, Ruben Kok, Joost Kok, Scott J. Lusher, Maryann E. Martone, Albert Mons, Abel L. Packer, Bengt Persson, Philippe Rocca-Serra, Marco Roos, Rene van Schaik, Susanna-Assunta Sansone, Erik Schultes, Thierry Sengstag, Ted Slater, George Strawn, Morris A. Swertz, Mark Thompson, Johan van der Lei, Erik van Mulligen, Jan Velterop, Andra Waagmeester, Peter Wittenburg, Katherine Wolstencroft, Jun Zhao, and Barend Mons. The FAIR guiding principles for scientific data management and stewardship. Scientific Data, 3, 2016. URL: https://doi.org/10.1038/sdata.2016.18.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact