Computer proofs about finite and regular sets: the unifying concept of subvariance

The work described here is a part of ongoing efforts to construct a set-theoretic framework that is convenient for automated reasoning in mathematics within first order logic. The specific topic in focus here is the theory of invariant and subvariant sets, which permits the development of a unified theory of regular and finite sets. Appendices are included listing theorems involving the axiom of regularity, the classes REGULAR and FINITE of regular sets and finite sets, respectively, as well as general theorems about invariant and subvariant subsets, all proved using McCune’s automated reasoning program Otter.