Source author record

Matt Kaufmann

Matt Kaufmann appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

9works
7topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

9 published item(s)

preprint2016arXiv

Largest initial segments pointwise fixed by automorphisms of models of set theory

Given a model $\mathcal{M}$ of set theory, and a nontrivial automorphism $j$ of $\mathcal{M}$, let $\mathcal{I}_{\mathrm{fix}}(j)$ be the submodel of $\mathcal{M}$ whose universe consists of elements $m$ of $\mathcal{M}$ such that $j(x)=x$ for every $x$ in the transitive closure of $m$ (where the transitive closure of $m$ is computed within $\mathcal{M}$). Here we study the class $\mathcal{C}$ of structures of the form $\mathcal{I}_{\mathrm{fix}}(j)$, where the ambient model $\mathcal{M}$ satisfies a frugal yet robust fragment of $\mathrm{ZFC}$ known as $\mathrm{MOST}$, and $j(m)=m$ whenever $m$ is a finite ordinal in the sense of $\mathcal{M}$. We show that every structure in $\mathcal{C}$ satisfies $\mathrm{MOST}+Δ_0^\mathcal{P}\textrm{-Collection}$. We also show that the following countable structures are in $\mathcal{C}$: (a) transitive models of $\mathrm{MOST}+Δ_0^\mathcal{P}\textrm{-Collection}$, (b) recursively saturated models of $\mathrm{MOST}+Δ_0^\mathcal{P}\textrm{-Collection}$, (c) models of $\mathrm{ZFC}$. It follows from (b) that the theory of $\mathcal{C}$ is precisely $\mathrm{MOST+Δ}_{0}^{\mathcal{P}}$-Collection. We conclude by proving a refinement of a result due to Amir Togha.

preprint2015arXiv

Fourier Series Formalization in ACL2(r)

We formalize some basic properties of Fourier series in the logic of ACL2(r), which is a variant of ACL2 that supports reasoning about the real and complex numbers by way of non-standard analysis. More specifically, we extend a framework for formally evaluating definite integrals of real-valued, continuous functions using the Second Fundamental Theorem of Calculus. Our extended framework is also applied to functions containing free arguments. Using this framework, we are able to prove the orthogonality relationships between trigonometric functions, which are the essential properties in Fourier series analysis. The sum rule for definite integrals of indexed sums is also formalized by applying the extended framework along with the First Fundamental Theorem of Calculus and the sum rule for differentiation. The Fourier coefficient formulas of periodic functions are then formalized from the orthogonality relations and the sum rule for integration. Consequently, the uniqueness of Fourier sums is a straightforward corollary. We also present our formalization of the sum rule for definite integrals of infinite series in ACL2(r). Part of this task is to prove the Dini Uniform Convergence Theorem and the continuity of a limit function under certain conditions. A key technique in our proofs of these theorems is to apply the overspill principle from non-standard analysis.

preprint2015arXiv

Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications

This volume contains the proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 2015, a two-day workshop held in Austin, Texas, USA, on October 1-2, 2015. ACL2 workshops occur at approximately 18-month intervals and provide a major technical forum for researchers to present and discuss improvements and extensions to the theorem prover, comparisons of ACL2 with other systems, and applications of ACL2 in formal verification. ACL2 is a state-of-the-art automated reasoning system that has been successfully applied in academia, government, and industry for specification and verification of computing systems and in teaching computer science courses. In 2005, Boyer, Kaufmann, and Moore were awarded the 2005 ACM Software System Award for their work on ACL2 and the other theorem provers in the Boyer-Moore family.

preprint2014arXiv

Industrial-Strength Documentation for ACL2

The ACL2 theorem prover is a complex system. Its libraries are vast. Industrial verification efforts may extend this base with hundreds of thousands of lines of additional modeling tools, specifications, and proof scripts. High quality documentation is vital for teams that are working together on projects of this scale. We have developed XDOC, a flexible, scalable documentation tool for ACL2 that can incorporate the documentation for ACL2 itself, the Community Books, and an organization's internal formal verification projects, and which has many features that help to keep the resulting manuals up to date. Using this tool, we have produced a comprehensive, publicly available ACL2+Books Manual that brings better documentation to all ACL2 users. We have also developed an extended manual for use within Centaur Technology that extends the public manual to cover Centaur's internal books. We expect that other organizations using ACL2 will wish to develop similarly extended manuals.

preprint2011arXiv

How Can I Do That with ACL2? Recent Enhancements to ACL2

The last several years have seen major enhancements to ACL2 functionality, largely driven by requests from its user community, including utilities now in common use such as 'make-event', 'mbe', and trust tags. In this paper we provide user-level summaries of some ACL2 enhancements introduced after the release of Version 3.5 (in May, 2009, at about the time of the 2009 ACL2 workshop) up through the release of Version 4.3 in July, 2011, roughly a couple of years later. Many of these features are not particularly well known yet, but most ACL2 users could take advantage of at least some of them. Some of the changes could affect existing proof efforts, such as a change that treats pairs of functions such as 'member' and 'member-equal' as the same function.

preprint2011arXiv

Integrating Testing and Interactive Theorem Proving

Using an interactive theorem prover to reason about programs involves a sequence of interactions where the user challenges the theorem prover with conjectures. Invariably, many of the conjectures posed are in fact false, and users often spend considerable effort examining the theorem prover's output before realizing this. We present a synergistic integration of testing with theorem proving, implemented in the ACL2 Sedan (ACL2s), for automatically generating concrete counterexamples. Our method uses the full power of the theorem prover and associated libraries to simplify conjectures; this simplification can transform conjectures for which finding counterexamples is hard into conjectures where finding counterexamples is trivial. In fact, our approach even leads to better theorem proving, e.g. if testing shows that a generalization step leads to a false conjecture, we force the theorem prover to backtrack, allowing it to pursue more fruitful options that may yield a proof. The focus of the paper is on the engineering of a synergistic integration of testing with interactive theorem proving; this includes extending ACL2 with new functionality that we expect to be of general interest. We also discuss our experience in using ACL2s to teach freshman students how to reason about their programs.