×
Author ID: kaufmann.matt Recent zbMATH articles by "Kaufmann, Matt"
Published as: Kaufmann, Matt; Kaufmann, M.

Publications by Year

Citations contained in zbMATH Open

43 Publications have been cited 265 times in 204 Documents Cited by Year
Model-theoretic logics. (Parts A-C). Zbl 0587.03001
108
1985
Stationary logic. Zbl 0372.02031
Barwise, Jon; Kaufmann, Matt; Makkai, Michael
33
1978
Model-theoretic logics. (Parts D-F). Zbl 0587.03002
26
1985
On random models of finite power and monadic logic. Zbl 0579.03006
Kaufmann, Matt; Shelah, Saharon
25
1985
Efficient certified RAT verification. Zbl 1494.68284
Cruz-Filipe, Luís; Heule, Marijn J. H.; Hunt, Warren A. jun.; Kaufmann, Matt; Schneider-Kamp, Peter
24
2017
Functional instantiation in first-order logic. Zbl 0755.68120
Boyer, Robert S.; Goldschlag, David M.; Kaufmann, Matt; Moore, J. Strother
15
1991
Structured theory development for a mechanized logic. Zbl 0971.03017
Kaufmann, Matt; Moore, J. Strother
14
2001
A rather classless model. Zbl 0359.02054
Kaufmann, Matt
14
1977
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
13
1998
Nonstandard analysis in ACL2. Zbl 0991.03018
Gamboa, Ruben A.; Kaufmann, Matt
12
2001
The strength of nonstandard methods in arithmetic. Zbl 0587.03048
Henson, C. Ward; Kaufmann, Matt; Keisler, H. Jerome
10
1984
Saturation and simple extensions of models of Peano arithmetic. Zbl 0557.03021
Kaufmann, Matt; Schmerl, James H.
10
1984
Efficient, verified checking of propositional proofs. Zbl 1483.68483
Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan
9
2017
A correction to ”Stationary logic”. Zbl 0457.03034
Barwise, Jon; Kaufmann, Matt; Makkai, Michael
8
1981
Blunt and topless end extensions of models of set theory. Zbl 0537.03024
Kaufmann, Matt
8
1983
Remarks on weak notions of saturation in models of Peano arithmetic. Zbl 0619.03027
Kaufmann, Matt; Schmerl, James H.
7
1987
Meta reasoning in ACL2. Zbl 1152.68522
Hunt, Warren A. jun.; Kaufmann, Matt; Krug, Robert Bellarmine; Moore, J. Strother; Smith, Eric Whitman
7
2005
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
7
2008
The Boyer-Moore prover and Nuprl: An experimental comparison. Zbl 0799.68169
Basin, David; Kaufmann, Matt
6
1991
Quantum-thermodynamical description of discrete non-equilibrium systems. Zbl 0801.73010
Muschik, W.; Kaufmann, M.
5
1994
An ACL2 tutorial. Zbl 1165.68461
Kaufmann, Matt; Moore, J. Strother
4
2008
Largest initial segments pointwise fixed by automorphisms of models of set theory. Zbl 1477.03152
Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri
4
2018
The Hanf number of stationary logic. Zbl 0614.03034
Shelah, Saharon; Kaufmann, Matt
4
1986
Rewriting with equivalence relations in ACL2. Zbl 1140.68029
Kaufmann, Matt; Moore, J. Strother
3
2008
Integrating external deduction tools with ACL2. Zbl 1183.68558
Kaufmann, Matt; Moore, J Strother; Ray, Sandip; Reeber, Erik
3
2009
A computational logic for Applicative Common LISP. Zbl 1066.68120
Kaufmann, Matt; Moore, J. Strother
3
2002
Different dynamics and entropy rates in quantum-thermodynamics. Zbl 1053.82516
Kato, A.; Kaufmann, M.; Muschik, W.; Schirrmeister, D.
3
2000
An extension of the Boyer-Moore theorem prover to support first-order quantification. Zbl 0784.68076
Kaufmann, Matt
3
1992
Mutually generic classes and incompatible expansions. Zbl 0586.03040
Kaufmann, Matt
2
1984
Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm. Zbl 0723.68072
Kaufmann, Matt
2
1991
Set theory with a filter quantifier. Zbl 0518.03007
Kaufmann, Matt
2
1983
Iterated ultrapowers for the masses. Zbl 1483.03024
Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri
2
2018
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
Filter logics: Filters on \(omega_ 1\). Zbl 0467.03030
Kaufmann, Matt
1
1981
On existence of \(Sigma_ n\) end extensions. Zbl 0467.03021
Kaufmann, Matt
1
1981
Rough diamond: an extension of equivalence-based rewriting. Zbl 1416.68165
Kaufmann, Matt; Moore, J Strother
1
2014
A note on the Hanf number of second-order logic. Zbl 0644.03021
Kaufmann, Matt
1
1985
Limited second-order functionality in a first-order setting. Zbl 1468.68291
Kaufmann, Matt; Moore, J Strother
1
2020
Proof pearl: Wellfounded induction on the ordinals up to \(\epsilon _{0}\). Zbl 1144.68361
Kaufmann, Matt; Slind, Konrad
1
2007
Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Zbl 1195.68009
1
2010
Proceedings of the thirteenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, October 1–2, 2015. Zbl 1490.68020
1
2015
Some key research problems in automated theorem proving for hardware and software verification. Zbl 1103.68800
Kaufmann, Matt; Moore, J. Stroother
1
2004
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
Limited second-order functionality in a first-order setting. Zbl 1468.68291
Kaufmann, Matt; Moore, J Strother
1
2020
Largest initial segments pointwise fixed by automorphisms of models of set theory. Zbl 1477.03152
Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri
4
2018
Iterated ultrapowers for the masses. Zbl 1483.03024
Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri
2
2018
Efficient certified RAT verification. Zbl 1494.68284
Cruz-Filipe, Luís; Heule, Marijn J. H.; Hunt, Warren A. jun.; Kaufmann, Matt; Schneider-Kamp, Peter
24
2017
Efficient, verified checking of propositional proofs. Zbl 1483.68483
Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan
9
2017
Proceedings of the thirteenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, October 1–2, 2015. Zbl 1490.68020
1
2015
Rough diamond: an extension of equivalence-based rewriting. Zbl 1416.68165
Kaufmann, Matt; Moore, J Strother
1
2014
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
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
7
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
3
2002
Structured theory development for a mechanized logic. Zbl 0971.03017
Kaufmann, Matt; Moore, J. Strother
14
2001
Nonstandard analysis in ACL2. Zbl 0991.03018
Gamboa, Ruben A.; Kaufmann, Matt
12
2001
Different dynamics and entropy rates in quantum-thermodynamics. Zbl 1053.82516
Kato, A.; Kaufmann, M.; Muschik, W.; Schirrmeister, D.
3
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
13
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.
5
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
15
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
2
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
4
1986
Model-theoretic logics. (Parts A-C). Zbl 0587.03001
108
1985
Model-theoretic logics. (Parts D-F). Zbl 0587.03002
26
1985
On random models of finite power and monadic logic. Zbl 0579.03006
Kaufmann, Matt; Shelah, Saharon
25
1985
A note on the Hanf number of second-order logic. Zbl 0644.03021
Kaufmann, Matt
1
1985
The strength of nonstandard methods in arithmetic. Zbl 0587.03048
Henson, C. Ward; Kaufmann, Matt; Keisler, H. Jerome
10
1984
Saturation and simple extensions of models of Peano arithmetic. Zbl 0557.03021
Kaufmann, Matt; Schmerl, James H.
10
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
8
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
On existence of \(Sigma_ n\) end extensions. Zbl 0467.03021
Kaufmann, Matt
1
1981
Stationary logic. Zbl 0372.02031
Barwise, Jon; Kaufmann, Matt; Makkai, Michael
33
1978
A rather classless model. Zbl 0359.02054
Kaufmann, Matt
14
1977
all top 5

Cited by 282 Authors

15 Kaufmann, Matt
14 Enayat, Ali
10 Shelah, Saharon
9 Heule, Marijn J. H.
8 Moore, J Strother
8 Schmerl, James H.
7 Zhukovskiĭ, Maksim Evgen’evich
4 Boldo, Sylvie
4 Compton, Kevin J.
4 Keisler, Howard Jerome
4 Lammich, Peter
4 Leth, Steven C.
4 McKenzie, Zachiri
4 Melquiond, Guillaume
4 Ray, Sandip
3 Bogaerts, Bart
3 Gamboa, Ruben A.
3 Hamkins, Joel David
3 Kolaitis, Phokion G.
3 Martín-Mateos, Francisco-Jesús
3 Ruiz-Reina, José-Luis
3 Tzouvaras, Athanassios
3 Väänänen, Jouko Antero
3 Wcisło, Bartosz
2 Alonso, José-Antonio
2 Baldwin, John T.
2 Basin, David A.
2 Berg, Jeremias
2 Biere, Armin
2 Brakensiek, Joshua
2 Bryant, Randal E.
2 Dillinger, Peter C.
2 Egorova, Alena N.
2 Gordon, Michael J. C.
2 Hella, Lauri T.
2 Henson, C. Ward
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 Zbigniew
2 Mackey, John
2 Makowsky, Johann-Andreas
2 Manolios, Panagiotis
2 Muller, Jean-Michel
2 Mundici, Daniele
2 Myreen, Magnus O.
2 Narváez, David E.
2 Nordström, Jakob
2 Paşca, Ioana
2 Popescu, Andrei
2 Russinoff, David M.
2 Seese, Detlef G.
2 Slivovsky, Friedrich
2 Smith, Stuart T.
2 Szabo, Manfred Egon
2 Treur, Jan
2 Vandesande, Dieter
2 Vardi, Moshe Ya’akov
2 Vroon, Daron
1 Aderhold, Markus
1 Akhmejanova, Margarita B.
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 Ayad, Ali
1 Baek, Seulkee
1 Barbosa, Haniel
1 Barrett, Clark W.
1 Bauereiß, Thomas
1 Ben-David, Shai
1 Bevier, William R.
1 Bierman, Gavin M.
1 Blanchette, Jasmin Christian
1 Bogan, Sebastian
1 Bonacina, Maria Paola
1 Bonnet, Edouard
1 Boyer, Robert S.
1 Brain, Martin
1 Briseid, Eyvind Martol
1 Bruce, Kim B.
1 Cantone, Domenico
1 Chamarthi, Harsh Raju
1 Chevillard, Sylvain
1 Chew, Leroy
1 Claessen, Koen
1 Clavel, Renaud
1 Clément, François
1 Cowles, John R.
1 Cox, Sean D.
1 Cruz-Filipe, Luís
1 Daumas, Marc
1 Davis, Jared
1 De Wulf, Wolf
...and 182 more Authors
all top 5

Cited in 54 Serials

26 Journal of Automated Reasoning
25 The Journal of Symbolic Logic
18 Annals of Pure and Applied Logic
10 Archive for Mathematical Logic
6 Proceedings of the American Mathematical Society
6 Formal Aspects of Computing
5 Transactions of the American Mathematical Society
5 Mathematical Logic Quarterly (MLQ)
5 The Bulletin of Symbolic Logic
4 Studia Logica
4 Information and Computation
3 Archiv für Mathematische Logik und Grundlagenforschung
3 Israel Journal of Mathematics
3 Notre Dame Journal of Formal Logic
3 Theoretical Computer Science
3 Doklady Mathematics
2 Fundamenta Mathematicae
2 Random Structures & Algorithms
2 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 ACM Transactions on Mathematical Software
1 Algebra Universalis
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 Statistics & Probability Letters
1 Journal of Symbolic Computation
1 Journal of the American Mathematical Society
1 SIAM Journal on Discrete Mathematics
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 The Journal of Artificial Intelligence Research (JAIR)
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 ACM Transactions on Computational Logic
1 Journal of Applied Logic
1 Acta Numerica
1 Logical Methods in Computer Science
1 The Review of Symbolic Logic
1 Philosophical Transactions A. Royal Society of London

Citations by Year