| Publication | Date of Publication | Type |
|---|
| Iteration in ACL2 | 2024-08-22 | Paper |
| Fourier series formalization in ACL2(r) | 2024-08-21 | Paper |
| Meta-extract: using existing facts in meta-reasoning | 2024-08-21 | Paper |
| A versatile, sound tool for simplifying definitions | 2024-08-21 | Paper |
| Integrating testing and interactive theorem proving | 2024-08-13 | Paper |
| How can I do that with ACL2? Recent enhancements to ACL2 | 2024-08-13 | Paper |
| Enhancements to ACL2 in versions 5.0, 6.0, and 6.1 | 2024-08-13 | Paper |
Limited second-order functionality in a first-order setting
Journal of Automated Reasoning | 2020-03-03 | Paper |
Iterated ultrapowers for the masses
Archive for Mathematical Logic | 2018-08-16 | Paper |
A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
IEEE Transactions on Computers | 2018-07-09 | Paper |
Largest initial segments pointwise fixed by automorphisms of models of set theory
Archive for Mathematical Logic | 2018-02-09 | Paper |
| Efficient, verified checking of propositional proofs | 2018-01-04 | Paper |
Efficient certified RAT verification
(available as arXiv preprint) | 2017-09-22 | Paper |
Rough diamond: an extension of equivalence-based rewriting
Interactive Theorem Proving | 2014-09-08 | Paper |
A parallelized theorem prover for a logic with parallel execution
Interactive Theorem Proving | 2013-08-07 | Paper |
The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
Journal of Automated Reasoning | 2011-06-03 | Paper |
Integrating external deduction tools with ACL2
Journal of Applied Logic | 2009-03-25 | Paper |
An ACL2 Tutorial
Lecture Notes in Computer Science | 2008-12-04 | Paper |
Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0
Lecture Notes in Computer Science | 2008-09-02 | Paper |
Rewriting with equivalence relations in ACL2
Journal of Automated Reasoning | 2008-06-11 | Paper |
Efficient execution in an automated reasoning environment
Journal of Functional Programming | 2008-01-18 | Paper |
Meta Reasoning in ACL2
Lecture Notes in Computer Science | 2006-07-06 | Paper |
| scientific article; zbMATH DE number 2177632 (Why is no real title available?) | 2005-06-21 | Paper |
| scientific article; zbMATH DE number 2101985 (Why is no real title available?) | 2004-09-22 | Paper |
Nonstandard analysis in ACL2
Journal of Automated Reasoning | 2002-02-19 | Paper |
Structured theory development for a mechanized logic
Journal of Automated Reasoning | 2001-02-18 | Paper |
Verification of Year 2000 conversion rules using the ACL2 theorem prover
International Journal on Software Tools for Technology Transfer. STTT | 2000-01-01 | Paper |
Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
Journal of Automated Reasoning | 1996-06-11 | Paper |
An extension of the Boyer-Moore theorem prover to support first-order quantification
Journal of Automated Reasoning | 1994-01-04 | Paper |
| scientific article; zbMATH DE number 88983 (Why is no real title available?) | 1993-01-16 | Paper |
| scientific article; zbMATH DE number 65529 (Why is no real title available?) | 1992-09-27 | Paper |
Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm
Journal of Automated Reasoning | 1991-01-01 | Paper |
Remarks on weak notions of saturation in models of Peano arithmetic
Journal of Symbolic Logic | 1987-01-01 | Paper |
The Hanf number of stationary logic
Notre Dame Journal of Formal Logic | 1986-01-01 | Paper |
On random models of finite power and monadic logic
Discrete Mathematics | 1985-01-01 | Paper |
A note on the Hanf number of second-order logic
Notre Dame Journal of Formal Logic | 1985-01-01 | Paper |
Some remarks on equivalence in infinitary and stationary logic
Notre Dame Journal of Formal Logic | 1984-01-01 | Paper |
A nonconservativity result on global choice
Annals of Pure and Applied Logic | 1984-01-01 | Paper |
Saturation and simple extensions of models of Peano arithmetic
Annals of Pure and Applied Logic | 1984-01-01 | Paper |
The strength of nonstandard methods in arithmetic
Journal of Symbolic Logic | 1984-01-01 | Paper |
Mutually generic classes and incompatible expansions
Fundamenta Mathematicae | 1984-01-01 | Paper |
On expandability of models of arithmetic and set theory to models of weak second-order theories
Fundamenta Mathematicae | 1984-01-01 | Paper |
Filter Logics on ω
Journal of Symbolic Logic | 1984-01-01 | Paper |
DEFINABLE ULTRAPOWERS AND ULTRAFILTERS OVER ADMISSIBLE ORDINALS
Mathematical Logic Quarterly | 1984-01-01 | Paper |
Blunt and topless end extensions of models of set theory
Journal of Symbolic Logic | 1983-01-01 | Paper |
Set theory with a filter quantifier
Journal of Symbolic Logic | 1983-01-01 | Paper |
Filter logics: Filters on ω1
Annals of Mathematical Logic | 1981-01-01 | Paper |
A correction to “stationary logic”
Annals of Mathematical Logic | 1981-01-01 | Paper |
| scientific article; zbMATH DE number 3732013 (Why is no real title available?) | 1981-01-01 | Paper |
Σ1-well-founded compactness
Annals of Mathematical Logic | 1980-01-01 | Paper |
A new omitting types theorem for L(Q)
Journal of Symbolic Logic | 1979-01-01 | Paper |
Stationary logic
Annals of Mathematical Logic | 1978-01-01 | Paper |
| A Rather Classless Model | 1977-01-01 | Paper |
