References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. Coq Development Team (2014): The Coq Proof Assistant: Reference Manual. Technical Report. INRIA.
  6. 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.
  7. Eclipse IDE. http://www.eclipse.org/.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. jEdit: Programmer's Text Editor. http://www.jedit.org/.
  16. C. Kaliszyk (2007): Web Interfaces for Proof Assistants. In: User Interfaces for Theorem Provers, pp. 49–61.
  17. 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.
  18. M. Kohlhase (2006): OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2). Lecture Notes in Artificial Intelligence 4180. Springer.
  19. 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.
  20. U. Norell (2005): The Agda WiKi. http://wiki.portal.chalmers.se/agda.
  21. L. Paulson (1994): Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science 828. Springer, doi:10.1007/BFb0030561.
  22. 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.
  23. 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.
  24. 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.
  25. F. Rabe (2014): A Generic Type Theory. See http://kwarc.info/frabe/Research/rabe_mmttypetheory_14.pdf.
  26. 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.
  27. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org