Automated Reasoning Service for HOL Light

Cezary Kaliszyk, Josef Urban. Automated Reasoning Service for HOL Light. In Jacques Carette, David Aspinall, Christoph Lange 0002, Petr Sojka, Wolfgang Windsteiger, editors, Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. Volume 7961 of Lecture Notes in Computer Science, pages 120-135, Springer, 2013. [doi]

@inproceedings{KaliszykU13,
  title = {Automated Reasoning Service for HOL Light},
  author = {Cezary Kaliszyk and Josef Urban},
  year = {2013},
  doi = {10.1007/978-3-642-39320-4_8},
  url = {http://dx.doi.org/10.1007/978-3-642-39320-4_8},
  researchr = {https://researchr.org/publication/KaliszykU13},
  cites = {0},
  citedby = {0},
  pages = {120-135},
  booktitle = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings},
  editor = {Jacques Carette and David Aspinall and Christoph Lange 0002 and Petr Sojka and Wolfgang Windsteiger},
  volume = {7961},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-39319-8},
}