References

  1. Public Repository for Alignments. Available at https://gl.mathhub.info/alignments/Public.
  2. M. Boespflug, Q. Carbonneaux & O. Hermant (2012): The λΠ-calculus modulo as a universal proof language. In: D. Pichardie & T. Weber: Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp. 28–43.
  3. Jacques Carette, William Farmer & Michael Kohlhase (2014): Realms: A Structure for Consolidating Knowledge about Mathematical Theories. In: Watt, pp. 252–266, doi:10.1007/978-3-319-08434-3. Available at http://kwarc.info/kohlhase/papers/cicm14-realms.pdf. MKM Best-Paper-Award.
  4. Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski & Florian Rabe (2011): Project Abstract: Logic Atlas and Integrator (LATIN). In: Davenport, pp. 289–291, doi:10.1007/978-3-642-22673-1. Available at https://kwarc.info/people/frabe/Research/CHKMR_latinabs_11.pdf.
  5. (2017): Intelligent Computer Mathematics. LNAI. Springer. In press.
  6. James Davenport, William Farmer, Florian Rabe & Josef Urban (2011): Intelligent Computer Mathematics. LNAI 6824. Springer Verlag, doi:10.1007/978-3-642-22673-1.
  7. Paul-Olivier Dehaye, Mihnea Iancu, Michael Kohlhase, Alexander Konovalov, Samuel Lelièvre, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry & Tom Wiesing (2016): Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach. In: Michael Kohlhase, Moa Johansson, Bruce Miller, Leonardo de Moura & Frank Tompa: Intelligent Computer Mathematics 2016, LNAI 9791. Springer, doi:10.1007/978-3-642-39320-4. Available at https://github.com/OpenDreamKit/OpenDreamKit/blob/master/WP6/CICM2016/published.pdf.
  8. William M. Farmer, Joshua D. Guttman & F. Javier Thayer (1993): IMPS: An Interactive Mathematical Proof System. Journal of Automated Reasoning 11(2), pp. 213–248, doi:10.1007/BF00881906.
  9. Thibault Gauthier & Cezary Kaliszyk (2014): Matching concepts across HOL libraries. In: Stephen Watt, James Davenport, Alan Sexton, Petr Sojka & Josef Urban: CICM, LNCS 8543. Springer Verlag, pp. 267–281, doi:10.1007/978-3-319-08434-3_20.
  10. Mihnea Iancu, Michael Kohlhase & Florian Rabe (2011): Translating the Mizar Mathematical Library into OMDoc format. KWARC Report. Jacobs University Bremen. Available at http://uniformal.github.io/doc/applications/LATIN/docs/Mizar2OMDoc-Report.pdf.
  11. Cezary Kaliszyk, Michael Kohlhase, Dennis Müller & Florian Rabe (2016): Aligning the Libraries of Formal Mathematical Systems. Available at http://kwarc.info/kohlhase/submit/alignments16.pdf. Submitted to CPP 2016.
  12. Michael Kohlhase, Thomas Koprucki, Dennis Müller & Karsten Tabelow (2017): Mathematical models as research data via flexiformal theory graphs. In: Intelligent Computer Mathematics (CICM) 2017, doi:10.1007/978-3-319-42432-3_53. Available at http://kwarc.info/kohlhase/papers/cicm17-models.pdf. In press.
  13. Michael Kohlhase, Dennis Müller, Sam Owre & Florian Rabe (2017): Making PVS Accessible to Generic Services by Interpretation in a Universal Format, doi:10.1007/978-3-319-08434-3. Available at http://kwarc.info/kohlhase/submit/itp17-pvs.pdf. Accepted at ITP 2017.
  14. Michael Kohlhase (2006): OMDoc – An open markup format for mathematical documents [Version 1.2]. LNAI 4180. Springer Verlag, doi:10.1007/11826095. Available at http://omdoc.org/pubs/omdoc1.2.pdf.
  15. Cezary Kaliszyk & Florian Rabe (2014): Towards Knowledge Management for HOL Light. In: Watt, pp. 357–372, doi:10.1007/978-3-319-08434-3_26. Available at http://kwarc.info/frabe/Research/KR_hollight_14.pdf.
  16. Michael Kohlhase & Florian Rabe (2016): QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge. Journal of Formalized Reasoning 9(1), pp. 201–234, doi:10.6092/issn.1972-5787/4570. Available at http://jfr.unibo.it/article/download/4570/5733.
  17. Michael Kohlhase, Florian Rabe & Claudio Sacerdoti Coen (2011): A Foundational View on Integration Problems. In: Davenport, pp. 107–122, doi:10.1007/978-3-642-22673-1. Available at http://kwarc.info/kohlhase/papers/cicm11-integration.pdf.
  18. The LATIN Logic Atlas. Available at https://gl.mathhub.info/MMT/LATIN.
  19. MathHub.info: Active Mathematics. Available at http://mathhub.info.
  20. Metamath Home page. Available at http://us.metamath.org.
  21. Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase & Florian Rabe (2017): Classification of Alignments between Concepts of Formal Mathematical Systems. In: Intelligent Computer Mathematics (CICM) 2017, doi:10.1007/978-3-540-71067-7_7. Available at http://kwarc.info/kohlhase/submit/cicm17-alignments.pdf. In press.
  22. MitM: The Math-in-the-Middle Ontology. Available at https://mathhub.info/MitM.
  23. MitM/Foundation. Available at https://gl.mathhub.info/MitM/Foundation.
  24. MitM/Interfaces. Available at https://gl.mathhub.info/MitM/interfaces.
  25. MitM/smglom. Available at https://gl.mathhub.info/MitM/smglom.
  26. Dennis Müller & Michael Kohlhase (2015): Understanding Mathematical Theory Formation via Theory Intersections in MMT. Available at http://cicm-conference.org/2015/fm4m/FMM_2015_paper_2.pdf.
  27. The OAF Project & System. Available at http://oaf.mathhub.info.
  28. Open Digital Research Environment Toolkit for the Advancement of Mathematics. Available at https://github.com/OpenDreamKit/OpenDreamKit/raw/master/Proposal/proposal-www.pdf.
  29. OpenDreamKit Open Digital Research Environment Toolkit for the Advancement of Mathematics. Available at http://opendreamkit.org.
  30. S. Owre, J. M. Rushby & N. Shankar (1992): PVS: A Prototype Verification System. In: D. Kapur: Proceedings of the 11th Conference on Automated Deduction, LNCS 607. Springer Verlag, Saratoga Springs, NY, USA, pp. 748–752, doi:10.1007/3-540-55602-8.
  31. Steven Obua & Sebastian Skalberg (2006): Importing HOL into Isabelle/HOL, pp. 298–302. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/11814771_27.
  32. Florian Rabe (2012): A Query Language for Formal Mathematical Libraries. In: Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel & Volker Sorge: Intelligent Computer Mathematics, LNAI 7362. Springer Verlag, pp. 142–157, doi:10.1007/978-3-642-31374-5_10.
  33. Florian Rabe (2014): How to Identify, Translate, and Combine Logics?. Journal of Logic and Computation, doi:10.1093/logcom/exu079.
  34. Florian Rabe & Michael Kohlhase (2013): A Scalable Module System. Information & Computation 0(230), pp. 1–54. Available at http://kwarc.info/frabe/Research/mmt.pdf.
  35. A. Trybulec & H. Blair (1985): Computer Assisted Reasoning with MIZAR. In: A. Joshi: Proceedings of the 9th International Joint Conference on Artificial Intelligence. Morgan Kaufmann, pp. 26–28.
  36. Stephan Watt, James Davenport, Alan Sexton, Petr Sojka & Josef Urban (2014): Intelligent Computer Mathematics. LNCS 8543. Springer, doi:10.1007/978-3-319-08434-3.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org