| Publication | Date of Publication | Type |
|---|
| Finding proofs in Tarskian geometry | 2017-07-10 | Paper |
| OTTER Proofs in Tarskian Geometry | 2014-09-26 | Paper |
| The Legacy of a Great Researcher | 2013-04-16 | Paper |
| A Fascinating Country in the World of Computing | 2008-02-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3433180 | 2007-04-27 | Paper |
| Double-negation elimination in some propositional logics | 2006-01-30 | Paper |
| Mechanizing Mathematical Reasoning | 2006-01-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4817210 | 2004-09-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4816538 | 2004-09-09 | Paper |
| Shortest axiomatizations of implicational S4 and S5 | 2004-05-27 | Paper |
| The strategy of cramming | 2003-06-09 | Paper |
| Short single axioms for Boolean algebra | 2003-04-28 | Paper |
| Hilbert's twenty-fourth problem | 2003-04-28 | Paper |
| Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus | 2003-04-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4792019 | 2003-02-09 | Paper |
| Finding missing proofs with automated reasoning | 2002-11-13 | Paper |
| A milestone reached and a secret revealed | 2002-01-07 | Paper |
| Conquering the Meredith single axiom | 2002-01-07 | Paper |
| Missing proofs found | 2002-01-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754068 | 2001-12-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754067 | 2001-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4761817 | 2001-02-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4443194 | 2001-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4443196 | 2001-01-01 | Paper |
| The hot list strategy | 1999-11-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4264737 | 1999-10-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4255507 | 1999-08-16 | Paper |
| Automating the search for elegant proofs | 1999-01-03 | Paper |
| The power of combining resonance with heat | 1997-06-10 | Paper |
| The application of automated reasoning to questions in mathematics and logic | 1997-05-13 | Paper |
| OTTER and the Moufang identity problem | 1997-01-27 | Paper |
| Searching for circles of pure proofs | 1995-12-20 | Paper |
| The problem of hyperparamodulation and nuclei | 1994-12-21 | Paper |
| The kernel strategy and its use for the study of combinatory logic | 1994-12-07 | Paper |
| The problem of hyperparamodulation | 1994-11-10 | Paper |
| Basic research problems: The problem of strategy and hyperresolution | 1994-08-31 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4296171 | 1994-06-16 | Paper |
| The problem of induction | 1994-04-12 | Paper |
| The problem of reasoning by case analysis | 1994-04-12 | Paper |
| The problem of automated theorem finding | 1994-03-20 | Paper |
| The problem of naming and function replacement | 1994-01-23 | Paper |
| The problem of reasoning by analogy | 1994-01-23 | Paper |
| The problem of selecting an approach based on prior success | 1994-01-23 | Paper |
| The problem of demodulator adjunction | 1993-12-20 | Paper |
| The problem of demodulating across argument and literal boundaries | 1993-12-20 | Paper |
| The problem of demodulation during inference rule application | 1993-12-10 | Paper |
| The problem of reasoning from inequalities | 1992-12-14 | Paper |
| The linked inference principle. I: The formal treatment | 1992-09-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3994754 | 1992-09-17 | Paper |
| Automated theorem proving and logic programming: a natural symbiosis | 1992-06-25 | Paper |
| The absence and the presence of fixed point combinators | 1991-01-01 | Paper |
| Basic research problems: The problem of choosing the representation, inference rule, and strategy | 1991-01-01 | Paper |
| The problem of choosing the type of subsumption to use | 1991-01-01 | Paper |
| Meeting the challenge of fifty years of logic | 1990-01-01 | Paper |
| The problem of finding a semantic strategy for focusing inference rules | 1990-01-01 | Paper |
| The problem of guaranteeing the existence of a complete set of reductions | 1989-01-01 | Paper |
| The problem of determining the size of a complete set of reductions | 1989-01-01 | Paper |
| The problem of finding an inference rule for set theory | 1989-01-01 | Paper |
| Erratum to ``A case study in automated theorem proving: finding sages in combinatory logic | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3804236 | 1988-01-01 | Paper |
| A case study in automated theorem proving: Finding sages in combinatory logic | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3829089 | 1984-01-01 | Paper |
| Unit Refutations and Horn Sets | 1974-01-01 | Paper |
| A theorem-proving language for experimentation | 1974-01-01 | Paper |
