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

DOI10.1007/978-3-319-20615-8_25zbMath1417.68212arXiv1505.01577OpenAlexW1751036247MaRDI QIDQ3453131

Kazuhisa Nakasho, Yasunari Shidama

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1505.01577

zbMATH Keywords

Mizarmathematical knowledge managementdocumentation generatorsearch system

Mathematics Subject Classification ID

Knowledge representation (68T30) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Related Items (2)

Cross-ratio in real vector space ⋮ An integrated web platform for the Mizar Mathematical Library

Uses Software

• MizarMode
• MoMM
• Mizar
• PIDE
• Isabelle/jEdit
• MML
• Isabelle/PIDE

Cites Work

• Unnamed Item
• Unnamed Item
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• Premise selection for mathematics by corpus analysis and kernel methods
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• A Brief Overview of Mizar
• A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
• Large Formal Wikis: Issues and Solutions
• Mathematical Knowledge Management
• Mathematical Knowledge Management

This page was built for publication: Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library