@inproceedings{TPS:HUG93,
author = "Peter Andrews and Matthew Bishop and Sunil Issar and Dan
          Nesmith and Frank Pfenning and Hongwei Xi",
title = {TPS: An Interactive and Automatic Tool for Proving Theorems
         of Type Theory},
booktitle = "Proceedings of 6th International Workshop on Higher Order
             Logic Theorem Proving and Its Applications (HUG '93)",
editor ="Jeffrey J. Joyce and Carl-Johan H. Seger",
series = "Lecture Notes in Computer Science",
volume = 780,
year = 1994,
month = "August",
pages = "366-370",
address = "Vancouver, Canada",
}