@Article{BP13,
    Author       = "Benzm{\"u}ller, C. and Paulson, L.",
    Year         = "2013",
    Title        = "{Quantified Multimodal Logics in Simple Type Theory}",
    Journal      = "Logica Universalis",
    Volume       = "7",
    Number       = "1",
    Pages        = "7-20",
    Publisher    = "Springer",
    Address      = "Berlin, Germany",
    Comment      = "TPTPRef"
}

@InProceedings{BP13-TFF1,
    Author       = "Blanchette, J. and Paskevich, A.",
    Year         = "2013",
    Title        = "{TFF1: The TPTP Typed First-order Form with Rank-1 Polymorphism}",
    Editor       = "Bonacina, M.P.",
    BookTitle    = "{Proceedings of the 24th International Conference on Automated Deduction}",
    Place        = "Lake Placid, USA",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "7898",
    Pages        = "414-420",
    Publisher    = "Springer",
    Address      = "Berlin, Germany",
    Comment      = "TPTPCite"
}