publication . Preprint . 2015

Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library

Nakasho, Kazuhisa; Shidama, Yasunari;
Open Access English
  • Published: 07 May 2015
Abstract
The purpose of this project is to collect symbol information in the Mizar Mathematical Library and manipulate it into practical and organized documentation. Inspired by the MathWiki project and API reference systems for computer programs, we developed a documentation generator focusing on symbols for the HTML-ized Mizar library. The system has several helpful features, including a symbol list, incremental search, and a referrer list. It targets those who use proof assistance systems, the volume of whose libraries has been rapidly increasing year by year.
Subjects
free text keywords: Computer Science - Mathematical Software, G.4
Related Organizations
Download from
18 references, page 1 of 2

1. Jesse Alama, Kasper Brink, Lionel Mamane, and Josef Urban: Large Formal Wikis: Issues and Solutions. Calculemus/MKM 2011. LNCS, vol. 6824, pp. 133-148. Springer (2011). [OpenAIRE]

2. Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, and Josef Urban: Licensing the Mizar Mathematical Library. Calculemus/MKM 2011. LNCS, vol. 6824, pp. 149-163. Springer (2011).

3. Jesse Alama, Tom Heskes, Daniel Kuhlwein, Evgeni Tsivtsivadze, and Josef Urban: Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. J. Autom. Reasoning 52(2): 191-213 (2014).

4. Grzegorz Bancerek and Piotr Rudnicki: Information Retrieval in MML. MKM 2003. LNCS, vol. 2594, pp. 119-132. Springer (2003).

5. Grzegorz Bancerek and Josef Urban: Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles. MKM 2004. LNCS, vol. 3119, pp. 44-57. Springer (2004).

6. Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz: Mizar in a Nutshell. J. Formalized Reasoning 3(2): 153-245 (2010).

7. Artur Kornilowicz: On Rewriting Rules in Mizar. J. Autom. Reasoning 50(2): 203- 210 (2013). [OpenAIRE]

8. Roman Matuszewski and Piotr Rudnicki: Mizar: the first 30 years. Mechanized Mathematics and Its Applications 4(1): 3-24, (2005).

9. Adam Naumowicz and Artur Kornilowicz: A Brief Overview of Mizar. TPHOLs 2009. LNCS, vol. 5674, pp. 67-72. Springer (2009).

10. Carst Tankink: PIDE for Asynchronous Interaction with Coq. UITP 2014: 73-83. [OpenAIRE]

11. Andrzej Trybulec, Artur Kornilowicz, Adam Naumowicz, and Krystyna Kuperberg: Formal Mathematics for Mathematicians - Foreward to the Special Issue. J. Autom. Reasoning 50(2): 119-121 (2013).

12. Josef Urban: XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. MKM 2005. LNCS, vol. 3863, pp. 346-360. Springer (2006).

13. Josef Urban: MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Applied Logic 4(4): 414-427 (2006).

14. Josef Urban: Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics. International Journal on Artificial Intelligence Tools 15(1): 109-130 (2006).

15. Josef Urban, Jesse Alama, Piotr Rudnicki, and Herman Geuvers: A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus 2010. LNCS, vol. 6167, pp. 455-469. Springer (2010). [OpenAIRE]

18 references, page 1 of 2
Abstract
The purpose of this project is to collect symbol information in the Mizar Mathematical Library and manipulate it into practical and organized documentation. Inspired by the MathWiki project and API reference systems for computer programs, we developed a documentation generator focusing on symbols for the HTML-ized Mizar library. The system has several helpful features, including a symbol list, incremental search, and a referrer list. It targets those who use proof assistance systems, the volume of whose libraries has been rapidly increasing year by year.
Subjects
free text keywords: Computer Science - Mathematical Software, G.4
Related Organizations
Download from
18 references, page 1 of 2

1. Jesse Alama, Kasper Brink, Lionel Mamane, and Josef Urban: Large Formal Wikis: Issues and Solutions. Calculemus/MKM 2011. LNCS, vol. 6824, pp. 133-148. Springer (2011). [OpenAIRE]

2. Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, and Josef Urban: Licensing the Mizar Mathematical Library. Calculemus/MKM 2011. LNCS, vol. 6824, pp. 149-163. Springer (2011).

3. Jesse Alama, Tom Heskes, Daniel Kuhlwein, Evgeni Tsivtsivadze, and Josef Urban: Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. J. Autom. Reasoning 52(2): 191-213 (2014).

4. Grzegorz Bancerek and Piotr Rudnicki: Information Retrieval in MML. MKM 2003. LNCS, vol. 2594, pp. 119-132. Springer (2003).

5. Grzegorz Bancerek and Josef Urban: Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles. MKM 2004. LNCS, vol. 3119, pp. 44-57. Springer (2004).

6. Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz: Mizar in a Nutshell. J. Formalized Reasoning 3(2): 153-245 (2010).

7. Artur Kornilowicz: On Rewriting Rules in Mizar. J. Autom. Reasoning 50(2): 203- 210 (2013). [OpenAIRE]

8. Roman Matuszewski and Piotr Rudnicki: Mizar: the first 30 years. Mechanized Mathematics and Its Applications 4(1): 3-24, (2005).

9. Adam Naumowicz and Artur Kornilowicz: A Brief Overview of Mizar. TPHOLs 2009. LNCS, vol. 5674, pp. 67-72. Springer (2009).

10. Carst Tankink: PIDE for Asynchronous Interaction with Coq. UITP 2014: 73-83. [OpenAIRE]

11. Andrzej Trybulec, Artur Kornilowicz, Adam Naumowicz, and Krystyna Kuperberg: Formal Mathematics for Mathematicians - Foreward to the Special Issue. J. Autom. Reasoning 50(2): 119-121 (2013).

12. Josef Urban: XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. MKM 2005. LNCS, vol. 3863, pp. 346-360. Springer (2006).

13. Josef Urban: MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Applied Logic 4(4): 414-427 (2006).

14. Josef Urban: Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics. International Journal on Artificial Intelligence Tools 15(1): 109-130 (2006).

15. Josef Urban, Jesse Alama, Piotr Rudnicki, and Herman Geuvers: A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus 2010. LNCS, vol. 6167, pp. 455-469. Springer (2010). [OpenAIRE]

18 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue