Matt Kaufmann

Available identifiers

zbMath Open kaufmann.mattWikidataQ6788881 ScholiaQ6788881MaRDI QIDQ230814

List of research outcomes

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

Research outcomes over time

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Matt Kaufmann