Large Formal Wikis: Issues and Solutions
From MaRDI portal
Publication:5200113
DOI10.1007/978-3-642-22673-1_10zbMath1335.68220arXiv1107.3209OpenAlexW2763053546WikidataQ56168714 ScholiaQ56168714MaRDI QIDQ5200113
Josef Urban, Jesse Alama, Kasper Brink, Lionel Elie Mamane
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1107.3209
Knowledge representation (68T30) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)
Related Items
Mizar: State-of-the-art and Beyond ⋮ Formalizing Physics: Automation, Presentation and Foundation Issues ⋮ Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ An integrated web platform for the Mizar Mathematical Library ⋮ Eliciting implicit assumptions of Mizar proofs by property omission ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Premise selection for mathematics by corpus analysis and kernel methods
Uses Software
Cites Work
- Intelligent computer mathematics. 10th international conference, AISC 2010, 17th symposium, Calculemus 2010, and 9th international conference, MKM 2010, Paris, France, July 5--10, 2010. Proceedings
- Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
- A Declarative Language for the Coq Proof Assistant
- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar
- Proviola: A Tool for Proof Re-animation
- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
- Developing the Algebraic Hierarchy with Type Classes in Coq
- Information Retrieval and Rendering with MML Query
- Mathematical Knowledge Management
