Some Applications of Formal Mathematics

The proof assistant is a powerful tool in formal methods. These programs allow the user to make formal mathematical statements and construct formal proofs. The connections with mathematics and logic provide motivation for a variety of problems. This dissertation applies formal mathematics to a selection of such problems. In Chapter 3 we establish methods to count the number of strong subtrees of height m
in a binary tree of height n. Chapter 4 adapts notions of largeness defined for sets of natural numbers for use with trees. We examine matrix-weighted graph termination in Chapter 5, isolate two conditions from the termination criterion, and discuss their location in the arithmetic hierarchy. In Chapter 6 we show that the decision sets of problems such as termination have no maximal recursively enumerable subsets, and we discuss the position of the “smallest” non-trivial index sets in the arithmetic hierarchy. Chapter 7 reports on research into the characterization of neural nets and the formal verification of their properties.