nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Translating the `IMPS` Theory Library to MMT/OMDoc

verfasst von : Jonas Betzendahl, Michael Kohlhase

Erschienen in: Intelligent Computer Mathematics

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The IMPS system by Farmer, Guttman and Thayer was an influential automated reasoning system, pioneering mechanisations of features like theory morphisms, partial functions with subsorts, and the little theories approach to the axiomatic method. It comes with a large library of formalised mathematical knowledge covering a broad spectrum of different fields. Since IMPS is no longer under development, this library is in danger of being lost. In its present form, it is also not compatible for use with any other mathematical system.

To remedy that, we formalise the logic of IMPS (LUTINS), and draw on both the original theory library source files as well as the internal data structures of the system to generate a representation in a modern knowledge management format. Using this approach, we translate the library to OMDoc/MMT and verify the result using type-checking in the MMT system against our implementation of LUTINS .

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel System Description: XSL-Based Translator of Mizar to LaTeX

Nächstes Kapitel Using the Isabelle Ontology Framework

[FGT98] gives the example of the algorithm for differentiating polynomials for this.

The meta-theory-relation connects theories that live on different meta-levels; e.g. domain knowledge to its logical foundation and conversely the logical foundation to the logical framework it is formalised in.

This formalisation is part of the LATIN foundations see https://gl.mathhub.info/MMT/LATIN/blob/master/source/foundations/imps/lutins.mmt.

Which – like the original IMPS system – are written in the T language – a dialect of Scheme – and are hence often referred to simply as “T-files” in the following sections.

Note that the theories shown here are all part of the library; they are not duplicates created by the process from Fig. 7.

[Bet18]

Betzendahl, J.: Translating the IMPS theory library to MMT/OMDoc. Master’s Thesis. Informatik, Universität Bielefeld, April 2018. https://gl.kwarc.info/supervision/MSc-archive/blob/master/2018/jbetzendahl/thesis_imps2omdoc.pdf

[Chu40]

Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56–68 (1940)MathSciNetCrossRef

[Cod+11]

Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F.: Project abstract: logic atlas and integrator (LATIN). In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 289–291. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22673-1_24. https://kwarc.info/people/frabe/Research/CHKMR_latinabs_11.pdf

[Far90]

Farmer, W.M.: A partial-function version of Church’s simple theory of types. J. Symb. Log. 55, 1269–1291 (1990)MathSciNetCrossRef

[Far93]

Farmer, W.M.: Theory interpretation in simple type theory. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol. 816, pp. 96–123. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58233-9_6CrossRef

[FGT92]

Farmer, W.M., Guttman, J.D., Javier Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_192CrossRef

[FGT98]

Farmer, W.M., Guttman, J.D., Javier Thayer, F.: The IMPS 2.0 Users Manual, 1st edn. The MITRE Corporation, Bedford (1998)

[HHP93]

Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143–184 (1993)MathSciNetCrossRef

[Ian+13]

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). https://doi.org/10.1007/s10817-012-9271-4MathSciNetCrossRefMATH

[Ian17]

Iancu, M.: Towards flexiformal mathematics. Ph.D. thesis. Bremen, Germany: Jacobs University (2017). https://opus.jacobs-university.de/frontdoor/index/index/docId/721

[Koh+17]

Kohlhase, M., Müller, D., Owre, S., Rabe, F.: Making PVS accessible to generic services by interpretation in a universal format. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 319–335. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_21. http://kwarc.info/kohlhase/submit/itp17-pvs.pdfCrossRef

[Koh06]

Kohlhase, M.: OMDoc – An Open Markup Format for Mathematical Documents [version 1.2]. LNCS (LNAI), vol. 4180. Springer, Heidelberg (2006). https://doi.org/10.1007/11826095. http://omdoc.org/pubs/omdoc1.2.pdfCrossRef

[KPU16]

Kaliszyk, C., Pąk, K., Urban, J.: Towards a Mizar environment for Isabelle: foundations and language. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th Conference on Certified Programs and Proofs (CPP 2016), pp. 58–65. ACM (2016). https://doi.org/10.1145/2854065.2854070

[KR14]

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 (LNAI), vol. 8543, pp. 357–372. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_26. http://kwarc.info/frabe/Research/KR_hollight_14.pdf

[KS10]

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–338. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_23CrossRef

[KW10]

Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307–322. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_22CrossRef

[LATIN]

The LATIN Logic Atlas. https://gl.mathhub.info/MMT/LATIN. Accessed 02 June 2017

[LFX]

MathHub MMT/LFX Git Repository. http://gl.mathhub.info/MMT/LFX. Accessed 15 May 2015

[Li02]

Li, Y.: IMPS to OMDoc translation. Bachelor’s Thesis. McMaster University, August 2002

[Mül+17]

Müller, D., Gauthier, T., Kaliszyk, C., Kohlhase, M., Rabe, F.: Classification of alignments between concepts of formal mathematical systems. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 83–98. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_7CrossRef

[OAF]

The OAF Project & System. http://oaf.mathhub.info. Accessed 23 April 2015

[OS06]

Obua, S., Skalberg, S.: Importing HOL into Isabelle/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 298–302. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_27CrossRef

[Rab14]

Rabe, F.: How to identify, translate, and combine logics? J. Log. Comput. 27(6), 1753–1798 (2014). https://doi.org/10.1093/logcom/exu079CrossRefMATH

[Rab18]

Rabe, F.: MMT: a foundation-independent logical framework (2018). https://kwarc.info/people/frabe/Research/rabe_mmtsys_18.pdf

[RK13]

Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230, 1–54 (2013). http://kwarc.info/frabe/Research/mmt.pdfMathSciNetCrossRef

[RKM17]

Rupprecht, M., Kohlhase, M., Müller, D.: A flexible, interactive theory-graph viewer. In: Kohlhase, A., Pollanen, M. (eds.) 12th Workshop on Mathematical User Interfaces, MathUI 2017 (2017). http://kwarc.info/kohlhase/papers/mathui17-tgview.pdf

[TMI]

Theorem Prover Museum - IMPS. https://github.com/theoremprovermuseum/imps. Accessed 28 April 2018

Titel: Translating the IMPS Theory Library to MMT/OMDoc
verfasst von: Jonas Betzendahl
Michael Kohlhase
Verlag: Springer International Publishing
Buch: Intelligent Computer Mathematics
Print ISBN: 978-3-319-96811-7

Electronic ISBN: 978-3-319-96812-4

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-96812-4_2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"