| TPS: A theorem-proving system for classical type theory PB Andrews, M Bishop, S Issar, D Nesmith, F Pfenning, H Xi Journal of automated reasoning 16, 321-353, 1996 | 205 | 1996 |
| Ω-MKRP: A proof development environment X Huang, M Kerber, M Kohlhase, E Melis, D Nesmith, J Richts, ... Automated Deduction—CADE-12: 12th International Conference on Automated …, 1994 | 83 | 1994 |
| The TPS theorem proving system PB Andrews, S Issar, D Nesmith, F Pfenning 9th International Conference on Automated Deduction: Argonne, Illinois, USA …, 1988 | 68 | 1988 |
| Keim: A toolkit for automated deduction X Huang, M Kerber, M Kohlhase, E Melis, D Nesmith, J Richts, ... Automated Deduction—CADE-12: 12th International Conference on Automated …, 1994 | 28 | 1994 |
| Presenting intuitive deductions via symmetric simplification F Pfenning, D Nesmith International Conference on Automated Deduction, 336-350, 1990 | 26 | 1990 |
| TPS: An interactive and automatic tool for proving theorems of type theory PB Andrews, M Bishop, S Issar, D Nesmith, F Pfenning, H Xi Higher Order Logic Theorem Proving and Its Applications: 6th International …, 1994 | 10 | 1994 |
| An application of Klop's counterexample to a higher-order rewrite system D Nesmith | 8 | 1999 |
| KEiM-Manual D Nesmith Version 0, 1992 | 8 | 1992 |
| Keim–Manual, Version 1.2 D Nesmith Universität des Saarlandes, Im Stadtwald, Saarbrücken, 1994 | 5 | 1994 |
| Guaranteeing correctness through the communication of checkable proofs (or: Would you really trust an automated reasoning system?) X Huang, M Kerber, M Kohlhase, D Nesmith, J Richts Proceedings of the CADE-Workshop on Metatheoretic Extensibility of Automated …, 1994 | 3 | 1994 |
| Die Beweisentwicklungsumgebung-Mkrp X Huang, M Kerber, M Kohlhase, E Melis, D Nesmith, J Richts, ... Informatik Forschung und Entwicklung 11 (1), 20-26, 1996 | 2 | 1996 |
| TPS user’s manual PB Andrews, CE Brown, M Bishop, S Issar, D Nesmith, F Pfenning, H Xi, ... | 1 | 2011 |
| ETPS User’s Manual F Pfenning, S Issar, D Nesmith, PB Andrews, H Xi, M Bishop, CE Brown | | 2010 |
| GRADER Manual S Issar, PB Andrews, F Pfenning, D Nesmith | | 2007 |
| Tps3 Programmer’s Guide PB Andrews, D Nesmith, F Pfenning, S Issar, H Xi, M Bishop, CE Brown, ... | | 2000 |
| Die Beweisentwicklungsumgebung Omega-MKRK M Kerber, X Huang, M Kohlhase, E Melis, D Nesmith, J Richts, ... | | 1999 |
| A Test for Evaluating the Practical Usefulness of Deduction Systems M Kerber, X Huang, M Kohlhase, D Nesmith, J Richts | | 1999 |
| A Test for Evaluating the X Huang, M Kerber, M Kohlhase, D Nesmith, J Richts | | |
| A Proof Development Environment X Huang, M Kerber, M Kohlhase, E Melis, D Nesmith, J Richts, ... | | |
| G uaranteeing Correctness X Huang, M Kerber, M Kohlhase, D Nesmith, J Richts | | |
Frank PfenningProfessor of Computer Science, Carnegie Mellon UniversityVerified email at cs.cmu.edu
