The TPS Theorem Proving System. - Peter B. Andrews; Sunil Issar; Dan Nesmith; Frank Pfenning (CADE, 1990)

Presenting Intuitive Deductions via Symmetric Simplification. - Frank Pfenning; Dan Nesmith (CADE, 1990)

TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. - Peter B. Andrews; Matthew Bishop; Sunil Issar; Dan Nesmith; Frank Pfenning; Hongwei Xi (HUG, 1993)

Omega-MKRP: A Proof Development Environment. - Xiaorong Huang; Manfred Kerber; Michael Kohlhase; Erica Melis; Dan Nesmith; Jörn Richts; Jörg H. Siekmann (CADE, 1994)

KEIM: A Toolkit for Automated Deduction. - Xiaorong Huang; Manfred Kerber; Michael Kohlhase; Erica Melis; Dan Nesmith; Jörn Richts; Jörg H. Siekmann (CADE, 1994)

Die Beweisentwicklungsumgebung Omega-MKRP. - Xiaorong Huang; Manfred Kerber; Michael Kohlhase; Erica Melis; Dan Nesmith; Jörn Richts; Jörg H. Siekmann (Inform. Forsch. Entwickl., 1996)

TPS: A Theorem-Proving System for Classical Type Theory. - Peter B. Andrews; Matthew Bishop; Sunil Issar; Dan Nesmith; Frank Pfenning; Hongwei Xi (J. Autom. Reason., 1996)