Michael O'Connor

Ph.D. (2008) Cornell University

First Position

Quantitative analyst at Jane Street Capital


Using Tree Automata to Investigate Intuitionistic Propositional Logic


Research Area



Intuitionistic logic is an important variant of classical logic, but it is not as well understood, even in the propositional case. In this thesis, we describe a faithful representation of intuitionistic propositional formulas as tree automata. This representation permits a number of consequences, including a characterization theorem for free Heyting algebras, which are the intutionistic analogue of free Boolean algebras, and a new algorithm for solving equations over intuitionistic propositional logic.