Abstract

The libraries of deduction systems are growing constantly, so much that knowledge management concerns are becoming increasingly urgent to address. However, due to time constraints and legacy design choices, there is barely any deduction system that can keep up with the MKM state of the art. HOL Light in particular was designed as a lightweight deduction system that systematically relegates most MKM aspects to external solutions — not even the list of theorems is stored by the HOL Light kernel.

We make the first and hardest step towards knowledge management for HOL Light: We provide a representation of the HOL Light library in a standard MKM format that preserves the logical semantics and notations but is independent of the system itself. This provides an interface layer at which independent MKM applications can be developed. Moreover, we develop two such applications as examples. We employ the MMT system and its interactive web browser to view and navigate the library. And we use the MathWebSearch system to obtain a search engine for it.

BibTeX

@inproceedings{CKFR-CICM14,
  author      = "Cezary Kaliszyk and Florian Rabe",
  title       = "Towards Knowledge Management for {HOL} Light",
  booktitle   = "Proceedings of the 7th Conference on Intelligent Computer
                 Mathematics",
  editor      = "Stephen Watt and James Davenport and Alan Sexton and
                 Petr Sojka and Josef Urban",
  series      = "Lecture Notes in Computer Science",
  volume      = 8543,
  pages       = "357--372",
  publisher   = "Springer-Verlag",
  year        = 2014,
  doi         = "10.1007/978-3-319-08434-3_26"
}