report.tex

\documentclass[12pt,a4paper]{article}
\input{latexmacros.tex}
\usepackage{dirtytalk}
\usepackage{amsmath,caption,booktabs}
\usepackage{tikz-cd}
\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]

\title{Intuitionistic Propositional Logic Tableaux in
Haskell}
\author{Valentino Filipetto \& Gian Marco Osso}
\date{\today}
\hypersetup{pdfauthor={Valentino Filipetto \& Gian Marco Osso}, pdftitle={My Report}}

\begin{document}

\maketitle

\begin{abstract}
We present an implementation in Haskell of a tableau-style proof system for the
implication-free fragment of intuitionistic propositional logic, drawing inspiration from a
preexisting implementation of classical first-order logic proposed here [3]. We also propose
a tableau prover for classical propositional logic, obtained via a minor modification of
the original one. These two can be used in conjunction to have experimental evidence of
Glivenko’s theorem.
\end{abstract}

\tableofcontents

\clearpage

\input{Theory.tex}

\input{lib/Formulas.lhs}

\input{lib/Tableau.lhs}

\input{lib/HelperFunctions.lhs}

\input{lib/Step.lhs}

\input{lib/Solve.lhs}

\input{lib/MyQuickCheck.lhs}

\input{Conclusion.tex}

\newpage

\addcontentsline{toc}{section}{Bibliography}
\bibliographystyle{alpha}
\bibliography{references.bib}
\end{document}