| Publication | Date of Publication | Type |
|---|
| Limited second-order functionality in a first-order setting | 2020-03-03 | Paper |
| Iterated ultrapowers for the masses | 2018-08-16 | Paper |
| A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program | 2018-07-09 | Paper |
| Largest initial segments pointwise fixed by automorphisms of models of set theory | 2018-02-09 | Paper |
| Efficient, verified checking of propositional proofs | 2018-01-04 | Paper |
| Efficient certified RAT verification | 2017-09-22 | Paper |
| Rough Diamond: An Extension of Equivalence-Based Rewriting | 2014-09-08 | Paper |
| A Parallelized Theorem Prover for a Logic with Parallel Execution | 2013-08-07 | Paper |
| The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 | 2011-06-03 | Paper |
| Integrating external deduction tools with ACL2 | 2009-03-25 | Paper |
| An ACL2 Tutorial | 2008-12-04 | Paper |
| Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0 | 2008-09-02 | Paper |
| Rewriting with equivalence relations in ACL2 | 2008-06-11 | Paper |
| Efficient execution in an automated reasoning environment | 2008-01-18 | Paper |
| Meta Reasoning in ACL2 | 2006-07-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3021914 | 2005-06-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4817211 | 2004-09-22 | Paper |
| Nonstandard analysis in ACL2 | 2002-02-19 | Paper |
| Structured theory development for a mechanized logic | 2001-02-18 | Paper |
| Verification of Year 2000 conversion rules using the ACL2 theorem prover | 2000-01-01 | Paper |
| Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem | 1996-06-11 | Paper |
| An extension of the Boyer-Moore theorem prover to support first-order quantification | 1994-01-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4016540 | 1993-01-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4012877 | 1992-09-27 | Paper |
| Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm | 1991-01-01 | Paper |
| Remarks on weak notions of saturation in models of Peano arithmetic | 1987-01-01 | Paper |
| The Hanf number of stationary logic | 1986-01-01 | Paper |
| On random models of finite power and monadic logic | 1985-01-01 | Paper |
| A note on the Hanf number of second-order logic | 1985-01-01 | Paper |
| Some remarks on equivalence in infinitary and stationary logic | 1984-01-01 | Paper |
| A nonconservativity result on global choice | 1984-01-01 | Paper |
| Saturation and simple extensions of models of Peano arithmetic | 1984-01-01 | Paper |
| On expandability of models of arithmetic and set theory to models of weak second-order theories | 1984-01-01 | Paper |
| DEFINABLE ULTRAPOWERS AND ULTRAFILTERS OVER ADMISSIBLE ORDINALS | 1984-01-01 | Paper |
| Mutually generic classes and incompatible expansions | 1984-01-01 | Paper |
| The strength of nonstandard methods in arithmetic | 1984-01-01 | Paper |
| Filter Logics on ω | 1984-01-01 | Paper |
| Blunt and topless end extensions of models of set theory | 1983-01-01 | Paper |
| Set theory with a filter quantifier | 1983-01-01 | Paper |
| A correction to “stationary logic” | 1981-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3919681 | 1981-01-01 | Paper |
| Filter logics: Filters on ω1 | 1981-01-01 | Paper |
| Σ1-well-founded compactness | 1980-01-01 | Paper |
| A new omitting types theorem for L(Q) | 1979-01-01 | Paper |
| Stationary logic | 1978-01-01 | Paper |
| A Rather Classless Model | 1977-01-01 | Paper |
