@InProceedings{Ben99, Author = "Benzm{\"u}ller, C.", Year = "1999", Title = "{Extensional Higher-order Paramodulation and RUE-Resolution}", Editor = "Ganzinger, H.", BookTitle = "{Proceedings of the 16th International Conference on Automated Deduction}", Place = "Trento, Italy", Series = "Lecture Notes in Artificial Intelligence", Number = "1632", Pages = "399-413", Publisher = "Springer", Address = "Berlin, Germany", Comment = "" } % Other possible matches are: @PhDThesis{Ben99-PhD, Author = "Benzm{\"u}ller, C.", Year = "1999", Title = "{Equality and Extensionality in Higher-Order Theorem Proving}", School = "Department of Computer Science, Saarland University", Address = "Saarbruecken, Germany", Comment = "TPTPRef" }