@InProceedings{BN10, Author = "B{\"o}hme, S. and Nipkow, T.", Year = "2010", Title = "{Sledgehammer: Judgement Day}", Editor = "Giesl, J. and Haehnle, R.", BookTitle = "{Proceedings of the 5th International Joint Conference on Automated Reasoning}", Place = "Edinburgh, United Kingdom", Series = "Lecture Notes in Artificial Intelligence", Number = "6173", Pages = "107-121", Comment = "TPTPRef" } % Other possible matches are: @InProceedings{BN10-ITP, Author = "Blanchette, J. and Nipkow, T.", Year = "2010", Title = "{Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder}", Editor = "Kaufmann, M. and Paulson, L.", BookTitle = "{Proceedings of the 1st International Conference on Interactive Theorem Proving}", Place = "Edinburgh, United Kingdom", Series = "Lecture Notes in Computer Science", Number = "6172", Pages = "131-146", Publisher = "Springer", Address = "Berlin, Germany", Comment = "" }