@article {Andrews:June 1996:0168-7433:321,
	author = "Andrews P.B.",
	author = "Bishop M.",
	author = "Issar S.",
	author = "Nesmith D.",
	author = "Pfenning F.",
	author = "Xi H.",
	title = "TPS: A Theorem-Proving System for Classical Type Theory",
	journal = "Journal of Automated Reasoning",
	volume = "16",
	year = "June 1996",
	abstract = "<P> This is description of {\bf TPS}, a theorem-proving system for classical type theory (Church's typed \lambda -calculus). {\bf TPS} has been designed to be a general research tool for manipulating wffs of first- and higher-order logic, and searching for proofs of such wffs interactively or automatically, or in a combination of these modes. An important feature of {\bf TPS} is the ability to translate between expansion proofs and natural deduction proofs. Examples of theorems that {\bf TPS} can prove completely automatically are given to illustrate certain aspects of {\bf TPS}'s behavior and problems of theorem proving in higher-order logic. </P>",
	pages = "321-353(33)",
	url = "http://www.ingentaconnect.com/content/klu/jars/1996/00000016/00000003/00081315"
}