In this thesis we consider two mostly disjoint topics in formal language theory that both involve the study and use of regular languages. The first topic lies in the intersection of automata theory and additive number theory. We introduce a method of producing results in additive number theory, relying on theorem-proving software and an approximation technique. As an example of the method, we prove that every natural number greater than 25 can be written as the sum of at most 3 natural numbers whose canonical base-2 representations have an equal number of 0's and 1's. We prove analogous results about similarly defined sets using the automata theory approach, but also give proofs using more ;;traditional;; approaches.The second topic is the study languages defined by criteria involving the number of occurrences of a particular pair of words within other words. That is, we consider languages of words z defined with respect to words x, y where z has the same number of occurrences (resp., fewer occurrences), (resp., fewer occurrences or the same number of occurrences) of x as a subword of z and y as a subword of z. We give a necessary and sufficient condition on when such languages are regular, and show how to check this condition efficiently. We conclude by briefly considering ideas tying the two topics together.