BibTeX Publications - Thibault Gauthier



@inproceedings{tgckju-lpar17,
  author    = {Thibault Gauthier and Cezary Kaliszyk and Josef Urban},
  title     = {{TacticToe}: Learning to Reason with {HOL4} Tactics},
  booktitle = {LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  editor    = {Thomas Eiter and David Sands},
  series    = {EPiC Series in Computing},
  volume    = {46},
  pages     = {125--143},
  year      = {2017},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}



@inproceedings{tgck-cpp15,
 author = {Gauthier, Thibault and Kaliszyk, Cezary},
 title = {Premise Selection and External Provers for {HOL}4},
 booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs},
 series = {CPP '15},
 year = {2015},
 isbn = {978-1-4503-3296-5},
 location = {Mumbai, India},
 pages = {49--57},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/2676724.2693173},
 doi = {10.1145/2676724.2693173},
 acmid = {2693173},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {automated reasoning, higher-order logic, hol4, premise selection},
} 


@inproceedings{tgck-lpar15,
  author    = {Thibault Gauthier and
               Cezary Kaliszyk},
  title     = {Sharing {HOL4} and {HOL L}ight Proof Knowledge},
  booktitle = {20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)},
  pages     = {372--386},
  year      = {2015},
  editor    = {Martin Davis and
               Ansgar Fehnker and
               Annabelle McIver and
               Andrei Voronkov},
  series    = {Lecture Notes in Computer Science},
  volume    = {9450},
  publisher = {Springer},
  doi       = {10.1007/978-3-662-48899-7},
}

@inproceedings{tgck-cicm14,
author = {Thibault Gauthier and Cezary Kaliszyk},
title = {Matching concepts across {HOL} libraries},
booktitle = {Proceedings of the 7th Conference on Intelligent Computer Mathematics (CICM'14)},
editor = {Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
series = "Lecture Notes in Computer Science",
volume = 8543,
pages = "267--281",
year = 2014,
doi = "10.1007/978-3-319-08434-3_20"
}

@inproceedings{PAAR-2014:Beagle_as_a_HOL4_external_ATP_method,
  author    = {Thibault Gauthier and Cezary Kaliszyk and Chantal Keller and Michael Norrish},
  title     = {Beagle as a HOL4 external ATP method},
  booktitle = {PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning},
  editor    = {Stephan Schulz and Leonardo De Moura and Boris Konev},
  series    = {EPiC Series in Computing},
  volume    = {31},
  pages     = {50-59},
  year      = {2015},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2040-557X}}