is implicitly $\exists$-quantified. 
\end{itemize}

Note that, if \texttt{:-} is regarded as $\leftarrow$, this is the opposite of
the implicit quantification in the specification. However, these rules match
the normal expectation for proof-style statements. For example:
\begin{itemize}
\item $\mathsf{nat}(X) -> \mathsf{add}(X,a,X)$ is equivalent to 
    $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,a,X)$.
\item $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land
    \mathsf{nat}(Z)$ is equivalent to $\forall X,Y: \mathsf{nat}(X) \land 
    \mathsf{nat}(Y) -> \exists Z: \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$.
\end{itemize}

Internally, when processing a proof tree, Arend maintains two sets of 
in-scope variables: \emph{universals} and \emph{existentials}. Universals are
................................................................................

(This presentation is based in part on that in \mcitet{pfenning2006logic}.)

It is interesting to directly compare the two implementations of unification
(one of the few modules which is semantically similar in both
implementations). Both systems implement the same algorithm. The Javascript 
implementation consists of
136 lines of non-comment code and is quite difficult to follow; the Prolog 
implementation requires only 69 lines,
an almost 50\% reduction! This despite the fact that the Prolog implementation
does \emph{not} use the built-in unification to simplify the algorithm at all;
it would be largely the same if only traditional assignment were used.


\subsection{Proof Checking}

The proof checker is implemented in approximately 450 lines of Prolog code. It
essentially implements the rules of the reasoning logic presented in figure
\ref{reasoning-rules}, by recursively checking the proof tree. That is, it
first checks the root node to ensure that the proof object is consistent with
the conclusion (antecedents and consequent) by ensuring that it has the correct
number and type of subproofs. The subproofs are then recursively checked,
working through the tree until the axiomatic rules are reached (or, in the 
case of an incomplete proof, a \texttt{hole} is found, indicating an unproved
................................................................................
\]
\[
\inference[By induction]
    {\inference[$->$R]
        {\inference[Case]
            {\inference[Add-$0$]
                {}
                {x = 0 |- \mathsf{add}(0,0,0)} & 
             \inference[Backchain]
                {\inference[IH]
                    {\assume{x = s(x'), \mathsf{nat}^\downarrow(x') |- \mathsf{nat}^\downarrow(x')}}
                    {x = s(x'), \mathsf{nat}^\downarrow(x') |- \mathsf{add}(x',0,x')}}
                {x = s(x'), \mathsf{nat}^\downarrow(x') |- \mathsf{add}(s(x'),0,s(x'))}}
            {\mathsf{nat}^\uparrow(x) |- \mathsf{add}(x,0,x)}}
        {\mathsf{nat}^\uparrow(x) -> \mathsf{add}(x,0,x)}}
    {\mathsf{nat}(x) -> \mathsf{add}(x,0,x)}
\]
(This example also demonstrates one of the flaws of the derivation proof format,
its insatiable appetite for horizontal space.)

    is implicitly $\exists$-quantified. 
\end{itemize}

Note that, if \texttt{:-} is regarded as $\leftarrow$, this is the opposite of
the implicit quantification in the specification. However, these rules match
the normal expectation for proof-style statements. For example:
\begin{itemize}
\item $\mathsf{nat}(X) -> \mathsf{add}(X,z,X)$ is equivalent to 
    $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,z,X)$.
\item $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land
    \mathsf{nat}(Z)$ is equivalent to $\forall X,Y: \mathsf{nat}(X) \land 
    \mathsf{nat}(Y) -> \exists Z: \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$.
\end{itemize}

Internally, when processing a proof tree, Arend maintains two sets of 
in-scope variables: \emph{universals} and \emph{existentials}. Universals are
................................................................................

(This presentation is based in part on that in \mcitet{pfenning2006logic}.)

It is interesting to directly compare the two implementations of unification
(one of the few modules which is semantically similar in both
implementations). Both systems implement the same algorithm. The Javascript 
implementation consists of
\lnum{136} lines of non-comment code and is quite difficult to follow; the Prolog 
implementation requires only \lnum{69} lines,
an almost \lnum{50\%} reduction! This despite the fact that the Prolog implementation
does \emph{not} use the built-in unification to simplify the algorithm at all;
it would be largely the same if only traditional assignment were used.


\subsection{Proof Checking}

The proof checker is implemented in approximately \lnum{450} lines of Prolog code. It
essentially implements the rules of the reasoning logic presented in figure
\ref{reasoning-rules}, by recursively checking the proof tree. That is, it
first checks the root node to ensure that the proof object is consistent with
the conclusion (antecedents and consequent) by ensuring that it has the correct
number and type of subproofs. The subproofs are then recursively checked,
working through the tree until the axiomatic rules are reached (or, in the 
case of an incomplete proof, a \texttt{hole} is found, indicating an unproved
................................................................................
\]
\[
\inference[By induction]
    {\inference[$->$R]
        {\inference[Case]
            {\inference[Add-$0$]
                {}
                {\mathsf{add}(0,0,0)} & 
             \inference[Backchain]
                {\inference[IH]
                    {\assume{\mathsf{nat}^\downarrow(x') |- \mathsf{nat}^\downarrow(x')}}
                    {\mathsf{nat}^\downarrow(x') |- \mathsf{add}(x',0,x')}}
                {\mathsf{nat}^\downarrow(x') |- \mathsf{add}(s(x'),0,s(x'))}}
            {\mathsf{nat}^\uparrow(x) |- \mathsf{add}(x,0,x)}}
        {\mathsf{nat}^\uparrow(x) -> \mathsf{add}(x,0,x)}}
    {\mathsf{nat}(x) -> \mathsf{add}(x,0,x)}
\]
(This example also demonstrates one of the flaws of the derivation proof format,
its insatiable appetite for horizontal space.)