J. Alama, K. Brink, L. Mamane & J. Urban (2011):
Large Formal Wikis: Issues and Solutions.
In: J. Davenport, W. Farmer, J. Urban & F. Rabe: Intelligent Computer Mathematics.
Springer,
pp. 133–148,
doi:10.1007/978-3-642-22673-1_10.
J. Alama, L. Mamane & J. Urban (2012):
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar.
In: J. Jeuring, J. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel & V. Sorge: Intelligent Computer Mathematics.
Springer,
pp. 1–16,
doi:10.1007/978-3-642-31374-5_1.
D. Aspinall (2000):
Proof General: A Generic Tool for Proof Development.
In: S. Graf & M. Schwartzbach: Tools and Algorithms for Construction and Analysis of Systems.
Springer,
pp. 38–42,
doi:10.1007/3-540-46419-0_3.
T. Bourke, M. Daum, G. Klein & R. Kolanski (2012):
Challenges and Experiences in Managing Large-Scale Proofs.
In: J. Jeuring, J. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel & V. Sorge: Intelligent Computer Mathematics.
Springer,
pp. 32–48,
doi:10.1007/978-3-642-31374-5_3.
Coq Development Team (2014):
The Coq Proof Assistant: Reference Manual.
Technical Report.
INRIA.
P. Dillinger, P. Manolios, D. Vroon & J. Strother Moore (2007):
ACL2s: The ACL2 Sedan.
In: S. Autexier & C. Benzmüller: Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006),
pp. 3–18.
Eclipse IDE.
http://www.eclipse.org/.
G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. Le Roux, A. Mahboubi, R. O'Connor, S. Ould Biha, I. Pasca, L. Rideau, A. Solovyev, E. Tassi & L. Théry (2013):
A Machine-Checked Proof of the Odd Order Theorem.
In: S. Blazy, C. Paulin-Mohring & D. Pichardie: Interactive Theorem Proving,
pp. 163–179,
doi:10.1007/978-3-642-39634-2_14.
R. Harper, F. Honsell & G. Plotkin (1993):
A framework for defining logics.
Journal of the Association for Computing Machinery 40(1),
pp. 143–184,
doi:10.1145/138027.138060.
J. Harrison (1996):
HOL Light: A Tutorial Introduction.
In: Proceedings of the First International Conference on Formal Methods in Computer-Aided Design.
Springer,
pp. 265–269,
doi:10.1007/BFb0031814.
F. Horozal, A. Iacob, C. Jucovschi, M. Kohlhase & F. Rabe (2011):
Combining Source, Content, Presentation, Narration, and Relational Representation.
In: J. Davenport, W. Farmer, F. Rabe & J. Urban: Intelligent Computer Mathematics.
Springer,
pp. 212–227,
doi:10.1007/978-3-642-22673-1_15.
F. Horozal, M. Kohlhase & F. Rabe (2012):
Extending MKM Formats at the Statement Level.
In: J. Campbell, J. Carette, G. Dos Reis, J. Jeuring, P. Sojka, V. Sorge & M. Wenzel: Intelligent Computer Mathematics.
Springer,
pp. 64–79,
doi:10.1007/978-3-642-31374-5_5.
M. Iancu, M. Kohlhase, F. Rabe & J. Urban (2013):
The Mizar Mathematical Library in OMDoc: Translation and Applications.
Journal of Automated Reasoning 50(2),
pp. 191–202,
doi:10.1007/s10817-012-9271-4.
M. Iancu & F. Rabe (2012):
(Work-in-Progress) An MMT-Based User-Interface.
In: C. Kaliszyk & C. Lüth: Workshop on User Interfaces for Theorem Provers.
jEdit: Programmer's Text Editor.
http://www.jedit.org/.
C. Kaliszyk (2007):
Web Interfaces for Proof Assistants.
In: User Interfaces for Theorem Provers,
pp. 49–61.
C. Kaliszyk & J. Urban (2013):
Automated Reasoning Service for HOL Light.
In: J. Carette, D. Aspinall, C. Lange, P. Sojka & W. Windsteiger: Intelligent Computer Mathematics.
Springer,
pp. 120–135,
doi:10.1007/978-3-642-39320-4_8.
M. Kohlhase (2006):
OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2).
Lecture Notes in Artificial Intelligence 4180.
Springer.
M. Kohlhase & I. Şucan (2006):
A Search Engine for Mathematical Formulae.
In: T. Ida, J. Calmet & D. Wang: Artificial Intelligence and Symbolic Computation.
Springer,
pp. 241–253,
doi:10.1007/11856290_21.
U. Norell (2005):
The Agda WiKi.
http://wiki.portal.chalmers.se/agda.
L. Paulson (1994):
Isabelle: A Generic Theorem Prover.
Lecture Notes in Computer Science 828.
Springer,
doi:10.1007/BFb0030561.
F. Pfenning & C. Schürmann (1999):
System Description: Twelf - A Meta-Logical Framework for Deductive Systems.
Lecture Notes in Computer Science 1632,
pp. 202–206,
doi:10.1007/3-540-48660-7_14.
F. Rabe (2012):
A Query Language for Formal Mathematical Libraries.
In: J. Campbell, J. Carette, G. Dos Reis, J. Jeuring, P. Sojka, V. Sorge & M. Wenzel: Intelligent Computer Mathematics.
Springer,
pp. 142–157,
doi:10.1007/978-3-642-31374-5_10.
F. Rabe (2013):
The MMT API: A Generic MKM System.
In: J. Carette, D. Aspinall, C. Lange, P. Sojka & W. Windsteiger: Intelligent Computer Mathematics.
Springer,
pp. 339–343,
doi:10.1007/978-3-642-39320-4_25.
F. Rabe (2014):
A Generic Type Theory.
See http://kwarc.info/frabe/Research/rabe_mmttypetheory_14.pdf.
F. Rabe & M. Kohlhase (2013):
A Scalable Module System.
Information and Computation 230(1),
pp. 1–54,
doi:10.1016/j.ic.2013.06.001.
M. Wenzel (2012):
Isabelle/jEdit - A Prover IDE within the PIDE Framework.
In: J. Jeuring, J. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel & V. Sorge: Intelligent Computer Mathematics,
pp. 468–471,
doi:10.1007/978-3-642-31374-5_38.