Michael O'Connor

Ph.D. (2008) Cornell University

First Position

Quantitative analyst at Jane Street Capital

Dissertation

Using Tree Automata to Investigate Intuitionistic Propositional Logic

Advisor

Richard A. Shore

Research Area

Logic

Abstract

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.