| Publication | Date of Publication | Type |
|---|
| The TPS theorem proving system | 2023-04-28 | Paper |
| On sets, types, fixed points, and checkerboards | 2019-01-10 | Paper |
| A Bit of History Related to Logic Based on Equality | 2015-11-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086769 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086772 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086773 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086774 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086778 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086779 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086786 | 2011-03-30 | Paper |
| TPS: A hybrid automatic-interactive system for developing proofs | 2007-02-20 | Paper |
| Mechanizing Mathematical Reasoning | 2006-01-10 | Paper |
| Herbrand Award acceptance speech | 2004-03-15 | Paper |
| An introduction to mathematical logic and type theory: To truth through proof. | 2002-10-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2751367 | 2002-08-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2723416 | 2001-07-05 | Paper |
| Where Not to Find the Critical Points of a Polynomial--Variation on a Putnam Theme | 1997-08-07 | Paper |
| TPS: A theorem-proving system for classical type theory | 1996-11-25 | Paper |
| More on the problem of finding a mapping between clause representation and natural-deduction representation | 1991-01-01 | Paper |
| On connections and higher-order logic | 1989-01-01 | Paper |
| The Classification of Surfaces | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3795649 | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4726218 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3343471 | 1984-01-01 | Paper |
| Theorem Proving via General Matings | 1981-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3880316 | 1980-01-01 | Paper |
| Sullivan's Minimal Models and Higher Order Whitehead Products | 1978-01-01 | Paper |
| The genus of a closed simply connected manifold | 1976-01-01 | Paper |
| Refutations by Matings | 1976-01-01 | Paper |
| Resolution and the consistency of analysis | 1974-01-01 | Paper |
| Provability in Elementary Type Theory | 1974-01-01 | Paper |
| General models, descriptions, and choice in type theory | 1972-01-01 | Paper |
| General models and extensionality | 1972-01-01 | Paper |
| Resolution in type theory | 1971-01-01 | Paper |
| On simplifying the matrix of a wff | 1968-01-01 | Paper |
| Resolution With Merging | 1968-01-01 | Paper |
| A transfinite type theory with type variables | 1965-01-01 | Paper |
| False lemmas in Herbrand | 1963-01-01 | Paper |
