Experiences from Exporting Major Proof Assistant Libraries
Tóm tắt
The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented great theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution, and our experiences will prove valuable to others undertaking such efforts.
Tài liệu tham khảo
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, Orlando (1975)
Anonymous: The QED Manifesto. In: A. Bundy (ed.) Automated Deduction, pp. 238–251. Springer (1994)
Asperti, A., Guidi, F., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: whelp. In: J.C. Filliâtre, C. Paulin-Mohring, B. Werner (eds.) Types for Proofs and Programs, International Workshop, TYPES 2004, Revised Selected Papers, No. 3839 in LNCS, pp. 17–32. Springer (2006)
Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: Crafting a Proof Assistant. In: T. Altenkirch, C. McBride (eds.) Types, pp. 18–32. Springer (2006)
Aspinall, D., Denney, E., Lüth, C.: A semantic basis for proof queries and transformations. In: Bjørner, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 92–106. Springer, Berlin (2012)
Assaf, A.: A framework for defining computational higher-order logics. PhD thesis, École Polytechnique (2015)
Assaf, A., Burel, G.: Holide. https://www.rocq.inria.fr/deducteam/Holide/index.html (2013)
Betzendahl, J., Kohlhase, M.: Translating the IMPS theory library to MMT/OMDoc. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds.) Intelligent Computer Mathematics, vol. 11006, pp. 7–22. Springer, Berlin (2018)
Boespflug, M., Burel, G.: CoqInE: Translating the calculus of inductive constructions into the lambda Pi-calculus Modulo. In: D. Pichardie, T. Weber (eds.) Proof Exchange for Theorem Proving.CEUR-WS (2012)
Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F.: Project abstract: logic atlas and integrator (LATIN). In: Davenport, J., Farmer, W., Rabe, F., Urban, J. (eds.) Intelligent Computer Mathematics, pp. 289–291. Springer, Berlin (2011)
Condoluci, A., Kohlhase, M., Müller, D., Rabe, F., Sacerdoti Coen, C., Wenzel, M.: Relational data across mathematical libraries. In: C. Kaliszyk, E. Brady, A. Kohlhase, C. Sacerdoti Coen (eds.) Intelligent Computer Mathematics, pp. 61–76. Springer, Berlin (2019)
Coq Development Team: The Coq Proof Assistant: Reference Manual. Technical report, INRIA (2015)
Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61(1–4), 423–453 (2018)
de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A., Middeldorp, A. (eds.) Automated Deduction, pp. 378–388. Springer, Berlin (2015)
Farmer, W., Guttman, J., Thayer, F.: Little Theories. In: D. Kapur (ed.) Conference on Automated Deduction, pp. 467–581 (1992)
Farmer, W., Guttman, J., Thayer, F.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 11(2), 213–248 (1993)
Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, pp. 327–342. Springer, Berlin (2009)
Gauthier, T., Kaliszyk, C.: Aligning concepts across proof assistant libraries. J. Symb. Comput. 90, 89–123 (2019)
Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O’Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A Machine-checked proof of the odd order theorem. In: S. Blazy, C. Paulin-Mohring, D. Pichardie (eds.) Interactive Theorem Proving, pp. 163–179. Springer (2013)
Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. http://arxiv.org/abs/1501.02155 (2014)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143–184 (1993)
Harrison, J.: HOL light: a tutorial introduction. In: Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, pp. 265–269. Springer (1996)
Horozal, F., Kohlhase, M., Rabe, F.: Extending MKM formats at the statement level. In: Campbell, J., Carette, J., Dos Reis, G., Jeuring, J., Sojka, P., Sorge, V., Wenzel, M. (eds.) Intelligent Computer Mathematics, pp. 64–79. Springer, Berlin (2012)
Hurd, J.: Open theory: package management for higher order logic theories. In: Reis, G.D., Théry, L. (eds.) Programming Languages for Mechanized Mathematics Systems, pp. 31–37. ACM, New York (2009)
Iancu, M.: Towards Flexiformal Mathematics. PhD thesis, Jacobs University Bremen (2017)
Iancu, M., Kohlhase, M., Rabe, F.: Translating the mizar mathematical library into OMDoc format. Technical Report KWARC Report-01/11, Jacobs University Bremen (2011)
Iancu, M., Kohlhase, M., Rabe, F., Urban, J.: The mizar mathematical library in OMDoc: translation and applications. J. Autom. Reason. 50(2), 191–202 (2013)
Kaliszyk, C., Kohlhase, M., Müller, D., Rabe, F.: A Standard for aligning mathematical concepts. In: A. Kohlhase, M. Kohlhase, P. Libbrecht, B. Miller, F. Tompa, A. Naummowicz, W. Neuper, P. Quaresma, M. Suda (eds.) Work in progress at CICM 2016, pp. 229–244. CEUR-WS.org (2016)
Kaliszyk, C., Krauss, A.: Scalable LCF-style proof translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving, pp. 51–66. Springer, Berlin (2013)
Kaliszyk, C., Pak, K.: Semantics of Mizar as an Isabelle object logic. J. Autom. Reason. 63(3), 557–595 (2019)
Kaliszyk, C., Rabe, F.: Towards knowledge management for HOL light. In: Watt, S., Davenport, J., Sexton, A., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics, pp. 357–372. Springer, Berlin (2014)
Kaliszyk, C., Urban, J.: HOL(y)hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5–22 (2015)
Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L. (eds.) Interactive Theorem Proving, pp. 307–322. Springer, Berlin (2010)
Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: SeL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010)
Kohlhase, M.: OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2). No. 4180 in Lecture Notes in Artificial Intelligence. Springer (2006)
Kohlhase, M., Müller, D., Owre, S., Rabe, F.: Making PVS accessible to generic services by interpretation in a universal format. In: Ayala-Rincon, M., Munoz, C. (eds.) Interactive Theorem Proving, pp. 319–335. Springer, Berlin (2017)
Kohlhase, M., Rabe, F.: QED reloaded: towards a pluralistic formal library of mathematical knowledge. J. Formal. Reason. 9(1), 201–234 (2016)
Kohlhase, M., Rabe, F., Wenzel, M.: Making Isabelle content accessible in knowledge representation formats. In: M. Bezem, A. Mahboubi (eds.) Proceedings of the 25th International Conference on Types for Proofs and Programs, TYPES 2019, Leibniz International Proceedings in Informatics (LIPIcs), vol. 175. Dagstuhl Publishing (2020). 10.4230/LIPIcs.TYPES.2019.1. https://drops.dagstuhl.de/opus/volltexte/2020/13065
Krauss, A., Schropp, A.: A Mechanized Translation from Higher-Order Logic to Set Theory. In: Kaufmann, M., Paulson, L. (eds.) Interactive Theorem Proving, pp. 323–338. Springer, Berlin (2010)
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Lewis, R.: An extensible ad hoc interface between Lean and Mathematica. In: C. Dubois, B.W. Paleo (eds.) Proof exchange for theorem proving. Electronic Proceedings in Theoretical Computer Science, , pp. 23–37 . Open Publishing Association (2017)
Li, Y.: IMPS to OMDoc translation. Bachelor’s Thesis, McMaster University (2002)
Müller, D.: Mathematical knowledge management across formal libraries. Ph.D. thesis, Informatics, FAU Erlangen-Nürnberg. https://opus4.kobv.de/opus4-fau/files/12359/thesis.pdf (2019)
Müller, D., Rabe, F., Kohlhase, M.: Theories as types. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) 9th International Joint Conference on Automated Reasoning. Springer. https://kwarc.info/kohlhase/papers/ijcar18-records.pdf (2018)
Müller, D., Rabe, F., Rothgang, C., Kohlhase, M.: Representing structural language features in formal meta-languages. In: C. Benzmüller, B. Miller (eds.) Intelligent Computer Mathematics (CICM) 2020, LNAI, vol. 12236, pp. 206–221. Springer. https://kwarc.info/kohlhase/papers/cicm20-features.pdf (2020)
Müller, D., Rabe, F., Sacerdoti Coen, C.: The Coq Library as a Theory Graph. In: C. Kaliszyk, E. Brady, A. Kohlhase, C. Sacerdoti Coen (eds.) Intelligent Computer Mathematics, pp. 171–186. Springer (2019)
Naumov, P., Stehr, M., Meseguer, J.: The HOL/NuPRL proof translator—a practical approach to formal interoperability. In: R. Boulton, P. Jackson (eds.) 14th International Conference on Theorem Proving in Higher Order Logics. Springer (2001)
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)
Obua, S., Adams, M., Aspinall, D.: Capturing hiproofs in HOL Light. In: MKM/Calculemus/DML, pp. 184–199 (2013)
Obua, S., Skalberg, S.: Importing HOL into Isabelle/HOL. In: Shankar, N., Furbach, U. (eds.) Automated Reasoning, vol. 4130. Springer, Berlin (2006)
Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: D. Kapur (ed.) 11th International Conference on Automated Deduction (CADE), pp. 748–752. Springer (1992)
Paulson, L.: Isabelle: The next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361–386. Academic Press, London (1990)
Paulson, L.: Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 828. Springer (1994)
Paulson, L., Coen, M.: Zermelo-Fraenkel Set Theory (1993). Isabelle distribution, ZF/ZF.thy
Rabe, F.: The MMT API: a generic MKM system. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) Intelligent Computer Mathematics, pp. 339–343. Springer, Berlin (2013)
Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230(1), 1–54 (2013)
Rahli, V., Cohen, L., Bickford, M.: A verified theorem prover backend supported by a monotonic library. In: G. Barthe, G. Sutcliffe, M. Veanes (eds.) Logic for Programming, Artificial Intelligence and Reasoning, pp. 564–582. EasyChair (2018)
RDF Core Working Group of the W3C: Resource Description Framework Specification (2004). http://www.w3.org/RDF/
Sacerdoti Coen, C.: A plugin to export Coq libraries to XML. In: K.C, E. Brady, A. Kohlhase, C. Sacerdoti Coen (eds.) Intelligent Computer Mathematics, pp. 243–257. Springer, Berlin (2019)
Schürmann, C., Stehr, M.: An executable formalization of the HOL/Nuprl connection in the metalogical framework Twelf. In: F. Baader, A. Voronkov (eds.) 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer (2004)
Thiré, F.: Sharing a library between proof assistants: reaching out to the HOL family. In: F. Blanqui, G. Reis (eds.) Logical Frameworks and Meta-Languages: Theory and Practice, pp. 57–71. EPTCS (2018)
Trybulec, A., Blair, H.: Computer assisted reasoning with MIZAR. In: A. Joshi (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26–28. Morgan Kaufmann (1985)
Urban, J.: Translating Mizar for first order theorem provers. In: A. Asperti, B. Buchberger, J. Davenport (eds.) Mathematical knowledge management, pp. 203–215. Springer (2003)
W3C: SPARQL Query Language for RDF (2008). http://www.w3.org/TR/rdf-sparql-query/