@ARTICLE{TPS96,
author = "Andrews, P. and Bishop, M. and Issar, S. and Nesmith, D. and
		  Pfenning, F. and Xi, H.",
title = {{TPS}: A theorem proving system for classical type theory},
journal = "Journal of Automated Reasoning",
volume = 16,
number = 3,
pages = "321--353",
year = 1996,
month = "June",
}