An Exploration of Automated Reasoning and Intuitionistic Logic using Coq

This paper explores the implementation of intuitionistic logic in the domain-specific language Coq. In doing so, it provides a broad overview of formal logic, non-classical logics, and important concepts in intuitionistic logic. The paper also introduces the reader to Coq and to various tools that allow one to customize Coq\u27s functioning