Miscellaneous documents of Matt Kaufmann
Some day this might be a decent web page. For now, it's just a place
to put miscellaneous stuff.
Demo (movie) of acl2-doc browser
- Links to a couple of logic papers, both by Ali Enayat, Matt
Kaufmann, and Zachiri
Ultrapowers for the Masses
Initial Segments Pointwise Fixed by Automorphisms of Models of Set
available here for download, but
note that this second online version is missing some symbols in some browsers).
Preprint of "Limited Second-Order
Functionality in a First-Order Setting"
Matt Kaufmann and J Strother Moore
Preprint of "Efficient, Verified Checking
of Propositional Proofs"
Marijn Heule, Warren Hunt, Jr., Matt Kaufmann, and Nathan Wetzler
Slides presented at ITP 2017
Using Existing Facts in Meta-reasoning", Matt Kaufmann and
Sol Swords. ACL2 Workshop 2017.
Burroughs ARC Technical Report 86-01: A Sound Theorem-Prover for a Higher-Order Functional Language