Abstract
Automated Theorem Proving (ATP) is a subfield of automated reasoning wherein a conjecture is formally proved from axioms using computational methods. ATP benefits greatly from heuristics that estimate which inferences, during a proof attempt, are most relevant for finding a proof. Machine learning has enjoyed great success in recent years, and is well suited for mining heuristics from data. Having good representations of logical formulae is a very important prerequisite to using machine learning for finding useful heuristics for ATP. This thesis explores some approaches to representing logical formulae as rooted ordered labeled directed acyclic graphs, as well as finding embeddings of these logical formulae graphs as vectors. Vector embeddings serve as an ideal representation of logical formulae for processing in machine learning models such as neural networks.