×

zbMATH — the first resource for mathematics

Kaufmann, Matt

Compute Distance To:
Author ID: kaufmann.matt Recent zbMATH articles by "Kaufmann, Matt"
Published as: Kaufmann, Matt; Kaufmann, M.
Documents Indexed: 49 Publications since 1977, including 1 Book

Publications by Year

Citations contained in zbMATH Open

37 Publications have been cited 212 times in 163 Documents Cited by Year
Stationary logic. Zbl 0372.02031
Barwise, Jon; Kaufmann, Matt; Makkai, Michael
30
1978
On random models of finite power and monadic logic. Zbl 0579.03006
Kaufmann, Matt; Shelah, Saharon
23
1985
Functional instantiation in first-order logic. Zbl 0755.68120
Boyer, Robert S.; Goldschlag, David M.; Kaufmann, Matt; Moore, J. Strother
13
1991
Structured theory development for a mechanized logic. Zbl 0971.03017
Kaufmann, Matt; Moore, J. Strother
13
2001
Nonstandard analysis in ACL2. Zbl 0991.03018
Gamboa, Ruben A.; Kaufmann, Matt
11
2001
Saturation and simple extensions of models of Peano arithmetic. Zbl 0557.03021
Kaufmann, Matt; Schmerl, James H.
9
1984
A rather classless model. Zbl 0359.02054
Kaufmann, Matt
9
1977
The strength of nonstandard methods in arithmetic. Zbl 0587.03048
Henson, C. Ward; Kaufmann, Matt; Keisler, H. Jerome
9
1984
A mechanically checked proof of the \(\mathrm{AMD}5_K86^{\mathrm{TM}}\) floating-point division program. Zbl 1392.68051
Moore, J. Strother; Lynch, Thomas W.; Kaufmann, Matt
8
1998
A correction to ”Stationary logic”. Zbl 0457.03034
Barwise, Jon; Kaufmann, Matt; Makkai, Michael
8
1981
Meta reasoning in ACL2. Zbl 1152.68522
Hunt, Warren A. jun.; Kaufmann, Matt; Krug, Robert Bellarmine; Moore, J. Strother; Smith, Eric Whitman
7
2005
Remarks on weak notions of saturation in models of Peano arithmetic. Zbl 0619.03027
Kaufmann, Matt; Schmerl, James H.
7
1987
Blunt and topless end extensions of models of set theory. Zbl 0537.03024
Kaufmann, Matt
7
1983
Efficient execution in an automated reasoning environment. Zbl 1128.68090
Greve, David A.; Kaufmann, Matt; Manolios, Panagiotis; Moore, J. Strother; Ray, Sandip; Ruiz-Reina, José Luis; Sumners, Rob; Vroon, Daron; Wilding, Matthew
6
2008
Efficient certified RAT verification. Zbl 06778406
Cruz-Filipe, Luís; Heule, Marijn J. H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter
6
2017
The Boyer-Moore prover and Nuprl: An experimental comparison. Zbl 0799.68169
Basin, David; Kaufmann, Matt
6
1991
An ACL2 tutorial. Zbl 1165.68461
Kaufmann, Matt; Moore, J. Strother
4
2008
Quantum-thermodynamical description of discrete non-equilibrium systems. Zbl 0801.73010
Muschik, W.; Kaufmann, M.
4
1994
Efficient, verified checking of propositional proofs. Zbl 06821857
Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan
3
2017
Integrating external deduction tools with ACL2. Zbl 1183.68558
Kaufmann, Matt; Moore, J. Strother; Ray, Sandip; Reeber, Erik
3
2009
Rewriting with equivalence relations in ACL2. Zbl 1140.68029
Kaufmann, Matt; Moore, J. Strother
3
2008
An extension of the Boyer-Moore theorem prover to support first-order quantification. Zbl 0784.68076
Kaufmann, Matt
3
1992
A computational logic for Applicative Common LISP. Zbl 1066.68120
Kaufmann, Matt; Moore, J. Strother
2
2002
Iterated ultrapowers for the masses. Zbl 06919824
Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri
2
2018
The Hanf number of stationary logic. Zbl 0614.03034
Shelah, Saharon; Kaufmann, Matt
2
1986
Mutually generic classes and incompatible expansions. Zbl 0586.03040
Kaufmann, Matt
2
1984
Set theory with a filter quantifier. Zbl 0518.03007
Kaufmann, Matt
2
1983
Proof pearl: Wellfounded induction on the ordinals up to \(\epsilon _{0}\). Zbl 1144.68361
Kaufmann, Matt; Slind, Konrad
1
2007
Largest initial segments pointwise fixed by automorphisms of models of set theory. Zbl 06836952
Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri
1
2018
Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm. Zbl 0723.68072
Kaufmann, Matt
1
1991
Filter logics: Filters on \(omega_ 1\). Zbl 0467.03030
Kaufmann, Matt
1
1981
Some key research problems in automated theorem proving for hardware and software verification. Zbl 1103.68800
Kaufmann, Matt; Moore, J. Stroother
1
2004
Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Zbl 1195.68009
Kaufmann, Matt (ed.); Paulson, Lawrence C. (ed.)
1
2010
The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4. Zbl 1216.68233
Gordon, Michael J. C.; Kaufmann, Matt; Ray, Sandip
1
2011
Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem. Zbl 0847.68106
Kaufmann, Matt; Pecchiari, Paolo
1
1996
Different dynamics and entropy rates in quantum-thermodynamics. Zbl 1053.82516
Kato, A.; Kaufmann, M.; Muschik, W.; Schirrmeister, D.
1
2000
A note on the Hanf number of second-order logic. Zbl 0644.03021
Kaufmann, Matt
1
1985
Iterated ultrapowers for the masses. Zbl 06919824
Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri
2
2018
Largest initial segments pointwise fixed by automorphisms of models of set theory. Zbl 06836952
Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri
1
2018
Efficient certified RAT verification. Zbl 06778406
Cruz-Filipe, Luís; Heule, Marijn J. H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter
6
2017
Efficient, verified checking of propositional proofs. Zbl 06821857
Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan
3
2017
The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4. Zbl 1216.68233
Gordon, Michael J. C.; Kaufmann, Matt; Ray, Sandip
1
2011
Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Zbl 1195.68009
Kaufmann, Matt; Paulson, Lawrence C.
1
2010
Integrating external deduction tools with ACL2. Zbl 1183.68558
Kaufmann, Matt; Moore, J. Strother; Ray, Sandip; Reeber, Erik
3
2009
Efficient execution in an automated reasoning environment. Zbl 1128.68090
Greve, David A.; Kaufmann, Matt; Manolios, Panagiotis; Moore, J. Strother; Ray, Sandip; Ruiz-Reina, José Luis; Sumners, Rob; Vroon, Daron; Wilding, Matthew
6
2008
An ACL2 tutorial. Zbl 1165.68461
Kaufmann, Matt; Moore, J. Strother
4
2008
Rewriting with equivalence relations in ACL2. Zbl 1140.68029
Kaufmann, Matt; Moore, J. Strother
3
2008
Proof pearl: Wellfounded induction on the ordinals up to \(\epsilon _{0}\). Zbl 1144.68361
Kaufmann, Matt; Slind, Konrad
1
2007
Meta reasoning in ACL2. Zbl 1152.68522
Hunt, Warren A. jun.; Kaufmann, Matt; Krug, Robert Bellarmine; Moore, J. Strother; Smith, Eric Whitman
7
2005
Some key research problems in automated theorem proving for hardware and software verification. Zbl 1103.68800
Kaufmann, Matt; Moore, J. Stroother
1
2004
A computational logic for Applicative Common LISP. Zbl 1066.68120
Kaufmann, Matt; Moore, J. Strother
2
2002
Structured theory development for a mechanized logic. Zbl 0971.03017
Kaufmann, Matt; Moore, J. Strother
13
2001
Nonstandard analysis in ACL2. Zbl 0991.03018
Gamboa, Ruben A.; Kaufmann, Matt
11
2001
Different dynamics and entropy rates in quantum-thermodynamics. Zbl 1053.82516
Kato, A.; Kaufmann, M.; Muschik, W.; Schirrmeister, D.
1
2000
A mechanically checked proof of the \(\mathrm{AMD}5_K86^{\mathrm{TM}}\) floating-point division program. Zbl 1392.68051
Moore, J. Strother; Lynch, Thomas W.; Kaufmann, Matt
8
1998
Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem. Zbl 0847.68106
Kaufmann, Matt; Pecchiari, Paolo
1
1996
Quantum-thermodynamical description of discrete non-equilibrium systems. Zbl 0801.73010
Muschik, W.; Kaufmann, M.
4
1994
An extension of the Boyer-Moore theorem prover to support first-order quantification. Zbl 0784.68076
Kaufmann, Matt
3
1992
Functional instantiation in first-order logic. Zbl 0755.68120
Boyer, Robert S.; Goldschlag, David M.; Kaufmann, Matt; Moore, J. Strother
13
1991
The Boyer-Moore prover and Nuprl: An experimental comparison. Zbl 0799.68169
Basin, David; Kaufmann, Matt
6
1991
Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm. Zbl 0723.68072
Kaufmann, Matt
1
1991
Remarks on weak notions of saturation in models of Peano arithmetic. Zbl 0619.03027
Kaufmann, Matt; Schmerl, James H.
7
1987
The Hanf number of stationary logic. Zbl 0614.03034
Shelah, Saharon; Kaufmann, Matt
2
1986
On random models of finite power and monadic logic. Zbl 0579.03006
Kaufmann, Matt; Shelah, Saharon
23
1985
A note on the Hanf number of second-order logic. Zbl 0644.03021
Kaufmann, Matt
1
1985
Saturation and simple extensions of models of Peano arithmetic. Zbl 0557.03021
Kaufmann, Matt; Schmerl, James H.
9
1984
The strength of nonstandard methods in arithmetic. Zbl 0587.03048
Henson, C. Ward; Kaufmann, Matt; Keisler, H. Jerome
9
1984
Mutually generic classes and incompatible expansions. Zbl 0586.03040
Kaufmann, Matt
2
1984
Blunt and topless end extensions of models of set theory. Zbl 0537.03024
Kaufmann, Matt
7
1983
Set theory with a filter quantifier. Zbl 0518.03007
Kaufmann, Matt
2
1983
A correction to ”Stationary logic”. Zbl 0457.03034
Barwise, Jon; Kaufmann, Matt; Makkai, Michael
8
1981
Filter logics: Filters on \(omega_ 1\). Zbl 0467.03030
Kaufmann, Matt
1
1981
Stationary logic. Zbl 0372.02031
Barwise, Jon; Kaufmann, Matt; Makkai, Michael
30
1978
A rather classless model. Zbl 0359.02054
Kaufmann, Matt
9
1977
all top 5

Cited by 210 Authors

14 Kaufmann, Matt
10 Shelah, Saharon
9 Enayat, Ali
8 Schmerl, James H.
7 Moore, J Strother
6 Zhukovskiĭ, Maksim Evgen’evich
4 Compton, Kevin J.
4 Keisler, Howard Jerome
4 Leth, Steven C.
4 Ray, Sandip
3 Boldo, Sylvie
3 Gamboa, Ruben A.
3 Kolaitis, Phokion G.
3 Lammich, Peter
3 Martín-Mateos, Francisco-Jesús
3 Melquiond, Guillaume
3 Ruiz-Reina, José-Luis
3 Tzouvaras, Athanassios
3 Väänänen, Jouko Antero
2 Alonso, José-Antonio
2 Baldwin, John T.
2 Basin, David A.
2 Biere, Armin
2 Dillinger, Peter C.
2 Egorova, Alena N.
2 Gordon, Michael J. C.
2 Hella, Lauri T.
2 Henson, C. Ward
2 Heule, Marijn J. H.
2 Hidalgo, María-José
2 Jonker, Catholijn M.
2 Kiesl, Benjamin
2 Kossak, Roman
2 Le Bars, Jean-Marie
2 Lelay, Catherine
2 Łełyk, Mateusz
2 Makowsky, Johann-Andreas
2 Manolios, Panagiotis
2 McKenzie, Zachiri
2 Mundici, Daniele
2 Paşca, Ioana
2 Popova, Svetlana Nikolaevna
2 Russinoff, David M.
2 Seese, Detlef G.
2 Smith, Stuart T.
2 Szabo, Manfred Egon
2 Treur, Jan
2 Vardi, Moshe Y.
2 Vroon, Daron
2 Wcisło, Bartosz
1 Aderhold, Markus
1 Alechina, Natasha
1 Alkassar, Eyad
1 Alviano, Mario
1 Andreev, P. V.
1 Appenzeller, Fred
1 Armand, Michaël
1 Arthan, Rob D.
1 Barwise, Kenneth Jon
1 Bauereiß, Thomas
1 Bevier, William R.
1 Bierman, Gavin M.
1 Blanchette, Jasmin Christian
1 Bogan, Sebastian
1 Brain, Martin
1 Briseid, Eyvind Martol
1 Bruce, Kim B.
1 Cantone, Domenico
1 Chamarthi, Harsh Raju
1 Chevillard, Sylvain
1 Clavel, Renaud
1 Clément, François
1 Cowles, John R.
1 Daumas, Marc
1 Davis, Jared
1 Dodaro, Carmine
1 D’silva, Vijay
1 Du, Hongwei
1 Duan, Zhenhua
1 Fagin, Ronald
1 Farmer, William M.
1 Faure, Germain
1 Fichte, Johannes Klaus
1 Filliâtre, Jean-Christophe
1 Fletcher, Peter
1 Fleury, Mathias
1 Geuvers, Jan Herman
1 Gordon, Andrew D.
1 Gordon, Evgeniĭ Izrail’evich
1 Gottliebsen, Hanne
1 Grégoire, Benjamin
1 Griggio, Alberto
1 Gutman, Aleksandr Efimovich
1 Guzicki, Wojciech
1 Haller, Leopold
1 Hamkins, Joel David
1 Hardy, Ruth
1 Harnik, Victor
1 Harrison, John
1 Hecher, Markus
...and 110 more Authors
all top 5

Cited in 45 Serials

23 The Journal of Symbolic Logic
23 Journal of Automated Reasoning
16 Annals of Pure and Applied Logic
8 Archive for Mathematical Logic
6 Proceedings of the American Mathematical Society
6 Formal Aspects of Computing
5 Transactions of the American Mathematical Society
5 The Bulletin of Symbolic Logic
4 Studia Logica
4 Information and Computation
4 Mathematical Logic Quarterly (MLQ)
3 Archiv für Mathematische Logik und Grundlagenforschung
3 Theoretical Computer Science
3 Doklady Mathematics
2 Israel Journal of Mathematics
2 Notre Dame Journal of Formal Logic
2 Random Structures & Algorithms
2 MSCS. Mathematical Structures in Computer Science
2 Higher-Order and Symbolic Computation
2 Journal of Mathematical Logic
2 Sādhanā
2 Mathematics in Computer Science
1 Information Processing Letters
1 Letters in Mathematical Physics
1 Fuzzy Sets and Systems
1 Journal of Combinatorial Theory. Series B
1 Synthese
1 Topology and its Applications
1 European Journal of Combinatorics
1 Journal of Symbolic Computation
1 Journal of the American Mathematical Society
1 Journal of Cryptology
1 Applied Intelligence
1 Applicable Algebra in Engineering, Communication and Computing
1 Formal Methods in System Design
1 Journal of Functional Programming
1 Annals of Mathematics and Artificial Intelligence
1 Computational & Mathematical Organization Theory
1 Journal of Combinatorial Optimization
1 Discrete Dynamics in Nature and Society
1 Foundations of Science
1 Theory and Practice of Logic Programming
1 Journal of Applied Logic
1 The Review of Symbolic Logic
1 Philosophical Transactions A. Royal Society of London

Citations by Year