Speaker: John Siratt
University of Notre Dame
Will give a PhD Defense entitled:
Some Applications of Formal Mathematics
Abstract: In this thesis we will apply formal mathematics to problems in formal methods. One powerful tool used is the proof assistant which implements some proof system in which the user can specify properties and construct proofs. These connections with mathematics and logic can present us with a wide variety of research questions. Motivated by a problem in proof complexity, we establish methods to count the number of strong subtrees of height m in a binary tree of height n, and adapt notions of largeness defined for sets of natural numbers to trees. We isolate two conditions from a problem in termination analysis and discuss their location in the arithmetic hierarchy. We show that the decision sets of problems such as termination (indeed, all cylindrical sets) have no maximal recursively enumerable subsets, and we bound the position of the "smallest'' non-trivial index sets in the arithmetic hierarchy. We close with a report on ongoing research into the characterization of neural nets, which includes the equivalence of ReLU-activated binary classifiers to an unquantified fragment of first order arithmetic.
Date: 06-24-2024
Time: 2:00 pm
Location: Zoom
Zoom URL: notredame.zoom.us/my/