Top

Published in:

2019 | OriginalPaper | Chapter

Interaction with Formal Mathematical Documents in Isabelle/PIDE

Author : Makarius Wenzel

Published in: Intelligent Computer Mathematics

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for interactive theorem proving in Isabelle. The well-established Archive of Formal Proofs (AFP) testifies the success of such applications of formalized mathematics in Isabelle/HOL. More recently, the scope of PIDE has widened towards languages that are not connected to logic and proof in Isabelle, but taken from a broader repertoire of mathematics on the computer. The present paper provides a general overview of the PIDE project and its underlying document model, with built-in parallel evaluation and asynchronous interaction. There is also some discussion of original aims and approaches, successes and failures, later changes to the plan, and ideas for the future.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

next chapter Beginners’ Quest to Formalize Mathematics: A Feasibility Study in Isabelle

https://isabelle.sketis.net/Isabelle_CICM2019.

http://mizar.org/library and http://mizar.org/fm.

https://isabelle.sketis.net/Isabelle_Naproche_CICM2019.

Aspinall, D.: Proof General: a generic tool for proof development. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 38–43. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_3CrossRefMATH

Aspinall, D., Lüth, C., Winterstein, D.: A framework for interactive proof. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM 2007. LNCS (LNAI), vol. 4573, pp. 161–175. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_15CrossRef

Barras, B., et al.: Pervasive parallelism in highly-trustable interactive theorem proving systems. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 359–363. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_29CrossRef

Bertot, Y., Théry, L.: A generic approach to building user interfaces for theorem provers. J. Symbolic Comput. 11 (1996)

Blanchette, J.C.: Hammering away: a user’s guide to Sledgehammer for Isabelle/HOL. Isabelle Documentation (2019)

Condoluci, A., Kohlhase, M., Müller, D., Rabe, F., Sacerdoti Coen, C., Wenzel, M.: Relational data across mathematical libraries. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) Intelligent Computer Mathematics, CICM 2019, LNAI 11617, pp. 61–76. Springer, Heidelberg (2019)

Eberl, M., Klein, G., Nipkow, T., Paulson, L., Thiemann, R. (eds.): The Archive of Formal Proofs (AFP). https://dblp.uni-trier.de/db/journals/afp

Frerix, S., Koepke, P.: Automatic proof-checking of ordinary mathematical texts. In: Workshop on Formal Mathematics for Mathematicians (FMM 2018). CICM Informal Proceedings (2018). https://www.cicm-conference.org/2018/infproc/paper13.pdf

Gordon, M., Milner, R., Morris, L., Newey, M.C., Wadsworth, C.P.: A metalanguage for interactive proof in LCF. In: Principles of programming languages (POPL) (1978)

10.

Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979). https://doi.org/10.1007/3-540-09724-4CrossRefMATH

11.

Lyaletski, A., Paskevich, A., Verchinine, K.: Theorem proving and proof verification in the system SAD. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 236–250. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27818-4_17CrossRefMATH

12.

Matthews, D., Wenzel, M.: Efficient parallel programming in Poly/ML and Isabelle/ML. In: ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010) (2010)

13.

Oppen, D.C.: Pretty printing. ACM Trans. Program. Lang. Syst. 2(4) (1980)

14.

Tankink, C.: PIDE for asynchronous interaction with Coq. In: Benzmüller, C., Woltzenlogel Paleo, B. (eds.) User Interfaces for Theorem Provers (UITP 2014), EPTCS, vol. 167 (2014). https://doi.org/10.4204/EPTCS.167.9MathSciNetCrossRef

15.

Wenzel, M.: Parallel proof checking in Isabelle/Isar. In: Dos Reis, G., Théry, L. (eds.) ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). ACM Digital Library (2009)

16.

Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 244–259. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22673-1_17CrossRef

17.

Wenzel, M.: Isabelle/Isar – a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof – Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10, no. 23. University of Białystok (2007)

18.

Wenzel, M.: On prover interaction and integration with Isabelle/Scala. In: Ball, T., Giesl, J., Hähnle, R., Nipkow, T. (eds.) Interaction versus Automation: the Two Faces of Deduction (Dagstuhl Seminar 09411). Schloss Dagstuhl, Germany, October 2009. http://drops.dagstuhl.de/portals/09411, https://files.sketis.net/Dagstuhl2009.pdf

19.

Wenzel, M.: Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit. In: Coen, C.S., Aspinall, D. (eds.) User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite Workshop. ENTCS, Elsevier, July 2010

20.

Wenzel, M.: Isabelle/jEdit – a prover IDE within the PIDE framework. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 468–471. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31374-5_38. https://arxiv.org/abs/1207.3441CrossRef

21.

Wenzel, M.: PIDE as front-end technology for Coq (2013). https://arxiv.org/abs/1304.6626

22.

Wenzel, M.: READ-EVAL-PRINT in parallel and asynchronous proof-checking. In: Kaliszyk, C., Lüth, C. (eds.) User Interfaces for Theorem Provers UITP 2012, EPTCS, vol. 118 (2013). https://doi.org/10.4204/EPTCS.118.4CrossRef

23.

Wenzel, M.: Shared-memory multiprocessing for interactive theorem proving. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 418–434. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_30CrossRefMATH

24.

Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515–530. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08970-6_33CrossRef

25.

Wenzel, M.: System description: Isabelle/jEdit in 2014. In: Benzmüller, C., Woltzenlogel Paleo, B. (eds.) User Interfaces for Theorem Provers, UITP 2014, EPTCS, July 2014. http://eptcs.web.cse.unsw.edu.au/paper.cgi?UITP2014:11

26.

Wenzel, M.: Further scaling of Isabelle technology. In: Isabelle Workshop 2018, Oxford, UK (2018). https://files.sketis.net/Isabelle_Workshop_2018/Isabelle_2018_paper_1.pdf

27.

Wenzel, M.: The Isabelle prover IDE after 10 years of development. In: Bauer, A., Escardó, M., Lumsdaine, P.L., Mahboubi, A. (eds.) Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). Schloss Dagstuhl, Germany, August 2018. https://www.dagstuhl.de/18341, https://sketis.net/2018/the-isabelle-prover-ide-after-10-years-of-development

28.

Wenzel, M.: Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. In: Masci, P., Monahan, R., Prevosto, V. (eds.) F-IDE Workshop 2018, Oxford, UK, no. 284. EPTCS (2018). http://eptcs.web.cse.unsw.edu.au/paper.cgi?FIDE2018.6CrossRef

29.

Wenzel, M.: Isabelle/PIDE after 10 years of development. In: User Interfaces for Theorem Provers, UITP 2018 (2018). https://sketis.net/wp-content/uploads/2018/08/isabelle-pide-uitp2018.pdf

30.

Wenzel, M.: Isabelle/jEdit. Isabelle Documentation (2019)

Title: Interaction with Formal Mathematical Documents in Isabelle/PIDE
Author: Makarius Wenzel
Publisher: Springer International Publishing
Book: Intelligent Computer Mathematics
Print ISBN: 978-3-030-23249-8

Electronic ISBN: 978-3-030-23250-4

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-23250-4_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner