Index: report/arend-report.pdf
==================================================================
--- report/arend-report.pdf
+++ report/arend-report.pdf
cannot compute difference between binary files
Index: report/arend-report.tex
==================================================================
--- report/arend-report.tex
+++ report/arend-report.tex
@@ -1350,12 +1350,12 @@
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) -> \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}
@@ -1426,20 +1426,20 @@
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
+\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 450 lines of Prolog code. It
+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,
@@ -1881,16 +1881,16 @@
\inference[By induction]
{\inference[$->$R]
{\inference[Case]
{\inference[Add-$0$]
{}
- {x = 0 |- \mathsf{add}(0,0,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'))}}
+ {\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,