\documentclass{article}

\usepackage{booktabs}
\usepackage{amsmath,amssymb,mathtools}
\usepackage{stmaryrd}
\usepackage{tikz}
\usepackage{forest}
\usepackage{logicproof}
\usepackage{ebproof}
\usepackage[capitalize,noabbrev]{cleveref}

%%%%%%% Some macros to help with the typesetting %%%%%%%%%%

%% Semantical truth values
\newcommand*{\TT}{1}
\newcommand*{\FF}{0}
%% Semantic brackets (Scott brackets)
\DeclarePairedDelimiter{\sem}{\llbracket}{\rrbracket}
%% Proof rule labels
\newcommand*{\PLabel}[1]{(#1)}
\newcommand*{\Ax}{\PLabel{Assum}}
\newcommand*{\IAnd}{\PLabel{$\land$-I}}
\newcommand*{\LEAnd}{\PLabel{$\land$-E$_1$}}
\newcommand*{\REAnd}{\PLabel{$\land$-E$_2$}}
\newcommand*{\IImpl}{\PLabel{$\to$-I}}
\newcommand*{\EImpl}{\PLabel{$\to$-E}}

%%%%%% End of local macros %%%%%%%

\title{Logic Homework 1}
\author{Name\\
  s1234567\\
  Studies%Informatica, I&E, Bioinformatica, Wiskunde, ...
}

\begin{document}

\maketitle

This document is a template for the homework assignments.
It includes all packages necessary to produce truth tables, parse trees, and proofs.

\section*{Question 1}
\paragraph{a)}

A table of logical connectives:
\begin{center}
  \begin{tabular}{l|c}
    Name & Connective \\\hline
    Conjunction (and) & $\land$ \\
    Disjunction (or) & $\lor$ \\
    Implication & $\to$ \\
    Negation & $\neg$ \\
    Absurdity (bottom) & $\bot$
  \end{tabular}
\end{center}

The following is shows a derivation of $p \land q \to r \vdash p \to q \to r$,
where $\Gamma = p \land q \to r, p, q$ in \textbf{proof tree style}.
\begin{equation*}
  \begin{prooftree}
    \infer0{}
    \infer1[\Ax]{\Gamma \vdash p \land q \to r}
    \infer0{}
    \infer1[\Ax]{\Gamma \vdash q}
    \infer0{}
    \infer1[\Ax]{\Gamma \vdash p}
    \infer2[\IAnd]{\Gamma \vdash p \land q}
    \infer2[\EImpl]{\Gamma \vdash r}
    \infer1[\IImpl]{p \land q \to r, p \vdash q \to r}
    \infer1[\IImpl]{p \land q \to r \vdash p \to q \to r}
  \end{prooftree}
\end{equation*}

\cref{mytable} shows the truth table of $(p \to \neg q) \to (q \lor \neg p)$
and all of its subformulas, as shown in Figure 1.8 on page 40 of [HR04].
The semantics of formulas can be written as $\sem{\varphi}_{v}$.
Semantical entailment is written $\Gamma \vDash \varphi$.

\begin{table}[ht]
    \centering
    \begin{tabular}[t]{cc|cccc|c}
        \toprule
        \rotatebox{90}{$p$}
        & \rotatebox{90}{$q$}
        & \rotatebox{90}{$\neg p$}
        & \rotatebox{90}{$\neg q$}
        & \rotatebox{90}{$p \to \neg q$}
        & \rotatebox{90}{$q \lor \neg p$}
        & \rotatebox{90}{$(p \to \neg q) \to (q \lor \neg p)$} \\
        \midrule
        \TT & \TT & \FF  & \FF  & \TT        & \TT         & \TT \\
        \TT & \FF & \FF  & \TT  & \TT        & \FF         & \FF \\
        \FF & \TT & \TT  & \FF  & \FF        & \TT         & \TT \\
        \FF & \FF & \TT  & \TT  & \TT        & \TT         & \TT \\
        \bottomrule
    \end{tabular}
    \caption{An example of a truth table for a more complex logical formula.}
    \label{mytable}
\end{table}

\cref{mytree} shows the parse tree of
$(((\neg p) \land q) \to (p \land (q \lor ( \neg r))))$, as shown in
Figure 1.3 on page 34 of [HR04].



\begin{figure}[ht]
  \centering
  \begin{forest}
    for tree={%
      draw,
      circle,
      l sep=1mm,
      s sep=10mm
    }
    [$\to$
      % (\neg p) \land q
      [$\land$
        [$\neg$ [$p$] ]
        [$q$]
      ]
      % p \land (q \lor ( \neg r))
      [$\land$
        [$p$]
        [$\lor$
          [$q$]
          [$\neg$ [$r$] ]
        ]
      ]
    ]
  \end{forest}
  \caption{A parse tree representing a well-formed formula.}
  \label{mytree}
\end{figure}

\end{document}
