Check-in [04f1cd0696]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Final draft of report. (Unless I think of something else to add...)
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:04f1cd06962f11344527d7f7f19230d82dce2a68
User & Date: andy 2015-04-18 21:14:05
Context
2015-04-20
09:52
Fixed a minor typo. Leaf check-in: adaef9d668 user: andy tags: trunk
2015-04-18
21:14
Final draft of report. (Unless I think of something else to add...) check-in: 04f1cd0696 user: andy tags: trunk
19:48
Penultimate draft of the report. After spell checking and such, this will become the final draft. check-in: 98924328ad user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to report/arend-report.pdf.

cannot compute difference between binary files

Changes to report/arend-report.tex.

319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
...
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
...
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
...
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
...
806
807
808
809
810
811
812
813

814
815
816
817
818
819
820
....
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
....
1233
1234
1235
1236
1237
1238
1239
1240



1241
1242
1243
1244
1245
1246
1247
....
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
....
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
....
1789
1790
1791
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
....
1902
1903
1904
1905
1906
1907
1908
1909

1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920

1921
1922
1923
1924
1925
1926
1927
....
1959
1960
1961
1962
1963
1964
1965
1966
1967
1968
1969
1970
1971
1972
1973
....
2026
2027
2028
2029
2030
2031
2032
2033
2034
2035
2036
2037
2038
2039
2040
2041
2042
2043
2044
2045
2046
2047
2048
2049
2050
    smaller parts, lemmas can be used, like functions, to abstract out 
    commonly-used subproofs, or to break down proofs that would otherwise be
    too large and unwieldy to understand. 

\item The lack of traditional negation eliminates some of the more-confusing 
    elements of traditional logic programming. In particular, Arend has nothing
    corresponding to ``negation as failure''; it is not possible in Arend to 
    know, in a computational sense, when a proposition $P$ fails. Thus reasoning
    in Arend is entirely about things that are known to be true, never about 
    things that are assumed to be false.
\end{itemize}

Visually, Arend presents proofs as trees of subproofs. A proof in this 
presentation has the form
\[
................................................................................
    will, if sufficiently ``smart'', be able to prove any theorem which a 
    human with near-infinite patience could prove. Proofs produced by automated
    theorem provers are often quite lengthy, some stretching into the 
    thousands-of-pages. Automated theorem provers must often employ 
    sophisticated heuristics in their proof search algorithms, to avoid the
    exponential run times that would otherwise be required.

\item \emph{Model checking} concerns the automatic checking of a given 
    model against a formal specification. For example, given a state
    machine as a model of a computational system, we may wish to verify that
    the system never enters some particular set of error states. Since model
    checking is only tangentially related to our subject, we will not discuss
    it further.

\item \emph{Proof assistants} aim to aid in the development and checking of
    formal proofs. While some systems only check proofs for completeness, more
    modern systems will typically also aid the user in the development of a
    proof. Recent examples 
    include Coq \mcitep{Coq:manual}, Twelf \mcitep{pfenning1999system}, and 
    Abella \mcitep{gacek08ijcar} Several element of Arend's design
    were influenced by Abella, most notably the use of a constructive two-level
    logic for describing and reasoning about systems. For a full history of the 
    development of computer-assisted proof systems, see 
    \mcitet{geuvers2009proof}.

\item More recently, several systems have emerged which try to bridge the gap
    between traditional functional programming and theorem proving. Systems
................................................................................
is the same as saying that $t$ is a proof of $P$. Under this view, proof 
checking is the same as type checking. Arend is not directly based on the
Curry-Howard isomorphism; although its proofs are terms, it does not check them
by computing their types, since terms in Arend are untyped. Nonetheless, we
believe that it should be possible to derive a consistent type system from
Arend's reasoning logic, which would support this interpretation. 

Proof assistants that present a graphical interface are surprisingly rare. 
While graphical ``wrappers'' exist for some systems (for example, 
ProofWeb\link{http://prover.cs.ru.nl/login.php} for Coq), 
these were not a part of the design of their underlying
systems. The only proof assistant of which we are aware which makes graphical
interaction as much an integral feature as Arend is HLM 
\mcitep{reichelt2010types}. Like Arend, HLM encourages direct manipulation
of in-progress proofs and is explicitly designed with that hope that it will
................................................................................
\begin{itemize}


\item \mcitet{kadoda1999desirable} present the results of a survey on the
    desirable user-interface features in an educational proof assistant. One
    surprising result they describe is a positive correlation between both
    the interactivity of a system, and its ability to work with explicit 
    proof trees, and the ``error-proneness'' of a system. This strikes us as a
     surprising
    result, as Arend is both interactive and works with explicit proof trees,
    and yet has virtually no error-proneness during the proof construction
    process, as users are limited strictly to those actions which will
    progress the proof in a valid way.\marginnote{It should be noted
    this author did not discover Kadoda's work until after Arend's design, with
    its emphasis on these features, was largely finalized.}
     However, several features which 
    Kadoda describes as being ``highly'' desirable are present in Arend: its
................................................................................
\subsection{Reasoning logic}

\newthought{Arend's reasoning logic} is closer to a full 
expression of first-order
intuitionistic logic, with extensions to support proofs by single-induction. 
The inference rules defining the reasoning logic are 
presented in Figure \ref{reasoning-rules}. It supports rightward implication 
($\rightarrow$), with the restriction that the premise cannot contain nested 

implications, only conjunctions, disjunctions, and atomic 
goals.\footnote{This restriction subsumes the \emph{stratification} 
restriction in Abella; stratification in some form is required to ensure 
monotonicity of the logic.} This implies that antecedents cannot contain
implications, since they cannot be added by $\rightarrow_R$, and are not allowed
in definitions in the specification logic.

................................................................................

\subsection{Proof representation}

Informally, the content of a derivation is relatively simple: a tree of 
\textsc{-Left} and/or \textsc{-Right} rule applications, drawn from the rules
of the reasoning logic in figure \ref{reasoning-rules}. In practice, a more
detailed representation is required, one which, in particular, necessitates the
use of \emph{explicit substitution}, rather than the implicit substitution that
would result from naive use of (for example) the system unification in Prolog.

For derivations purely derived from the specification language, explicit 
substitution is not required. This is because for any valid derivation of a
proposition expressed in the specification language, the substitution is 
\emph{consistent} throughout the derivation tree; it is not possible for 
different ``branches'' to have different substitutions. (Disjunction may, of
course, result in the generation of multiple distinct derivations, each with its
own unifying substitution, but within any single derivation there is always a
single consistent substitution.)
................................................................................
would need to have a conclusion $X = z \land X = s(x')$, which is already 
inconsistent, and actually impossible to express, because Horn clauses forbid
such conjunctions as conclusions. Conversely, given the conclusion 
$X = z \lor X = s(x')$ we have
the choice of which unification to use, and thus there is no inconsistency.}

Because of this, each branch of a derivation must maintain its own substitution,
applied to its goals as they are expanded.




Proofs are represented as a term of the form
\begin{verbatim}
proof(Goal,Ctx,Subst,Proof)
\end{verbatim}
where \texttt{Goal} is the goal to be proved, \texttt{Ctx} is the list of
antecedents (initially empty for most goals), \texttt{Subst} is the 
................................................................................
    various -Left rules of the reasoning logic.
\item \texttt{trivial} --- Proves $\top$.
\item \texttt{hole} --- Proves any goal, but represents an incomplete proof.
\end{itemize}

\subsection{Capture avoidance}

The use of explicit substitution means that the proof-checker must also contend
with another troublesome problem which Prolog conceals: avoiding \emph{accidental
capture} when expanding a call to a goal. Consider the goal $\mathsf{nat}(X)$.
We would expect this goal to succeed twice, first with the solution $X = z$. 
However, if we naively unify this goal with the head of the Nat-Succ rule we
get the solution $X = s(X)$ which fails the occurs check. The problem is that
$X$ as present in our goal is not the same variable as $X$ in the Nat-Succ rule.
Variables in rule definitions are \emph{schematic}, their names should be
................................................................................
In this mode it can prove any proposition in the pure specification logic, and
even a few that lie outside it; these extensions include:
\begin{itemize}
\item Simple implications: for example, $P -> P$ can be proved.
\item Proofs involving $\bot$-Left, for example $\bot -> P$. 
\item Proofs involving limited use of other -Left rules. For example, 
    $P \land Q -> P$ can be proved.\footnote{$P \land Q -> P$ produces an 
    infinite sequence of proofs, because the list of premises, while properly
    speaking a set, is implemented as a list without duplicate removal, for
    efficiency reasons. Thus it is always possible to case on $P \land Q$, 
    keep the original premise, and thus generate an infinite collection of 
    $P$'s, each of which gives, theoretically, a distinct proof.}
\end{itemize}

More interestingly, \texttt{check} can be called with the \emph{goal} unbound
and the proof bound, albeit for a very limited set of proofs. In this mode it
will construct a proposition which is proved by the given proof. 
This behavior is not unexpected; by the Curry-Howard isomorphism proofs are 
................................................................................
\end{lstlisting}

with the (internal) restriction that the IH will never be used without explicit
action on the part of the user. Lemmas, once proved, are represented similarly,
as new program clauses, but requiring explicit use.

A somewhat unfamiliar aspect of Arend's use of induction is how the inductive
hypothesis is applied: ordinarily we would specify those premises of the current
proof state which matched the corresponding premises of the IH (i.e., 
``apply IH to $nat^\downarrow(X')$''); this would have the effect of introducing
the IH, with the appropriate substitutions, as a new premise, where the 
assumption rule could then use it to prove the conclusion.
Purely for user-interface reasons, we
apply the IH by backchaining it against the current \emph{conclusion}, replacing
the goal with the conjunction of the premises of the IH (again, with the
appropriate substitutions). The user can then use the $\land$-R rule to 
split the proof into subproofs with atomic goals, each of which can be proved
by the assumption rule.

The inductive hypothesis is used within a proof by backchaining on the current
goal, which must unify with the head of the IH. Recall that backchaining 
replaces the goal with its definition(s). Ordinarily the disjunction of 
................................................................................
\item Currently Arend allows specification authors minimal influence on the
    \emph{user interface}; their power is limited to declaratively describing
    how certain predicates should be rendered as HTML. For more complex
    specifications, this is insufficient. As an example, classical logic can
    be specified in Arend with relative ease, via a predicate \texttt{solve}:
    \texttt{solve(C,G,T)} succeeds if the proposition $G$ evaluates to the
    truth value $T$ in context $C$. However, none of the familiar operations
    for manipulating the goal and premises can be used with this specification,

    as they are ``hidden'' inside the arguments to a predicate. A system 
    allowing specification authors to highlight terms in various contexts as
    targets for user-manipulation would greatly extend the ease-of-use of the
    system when dealing with non-trivial specifications.

\item Many proof assistants allow the user to create \emph{tacticals}, 
    ``shortcuts'' through the proof process or alternate reasoning strategies.
    A cursory glance at the \emph{check/3} predicate at the heart of Arend's
    proof-checking algorithm will reveal a significant amount of similarity
    between the various cases: to apply a -Left or -Right rule, we apply
    some kind of transformation(s) to either one of the premises or the goal,

    and then recursively check zero or more of these transformed subproofs.
    Tacticals allow the user to specify these transformations themselves, in
    a way that enforces their consistency with the underlying logic. For
    some specifications, tacticals could significantly simplify the development
    of otherwise-tedious proofs, by concealing the irrelevant details.

\item In a similar vein, Arend currently requires the user to proceed through
................................................................................
    creating an ecosystem around student-created specifications, proofs, and 
    lemmas, perhaps with collaboration features for multi-student use.

\item Although we believe Arend's derivation-tree presentation of proofs has
    distinct advantages over the traditional paragraph format, there is no
    reason why an alternate user interface could not present proofs in that
    form, allowing users who feel more comfortable with a textual presentation
    to navigate their proofs in that way. Indeed, users could easily switch 
    between the two presentations, and any other future presentations that 
    might be added, even in the middle of a proof. Indeed, given the 
    hierarchical structure of proofs, it is entirely possible that the two
    notations could be mixed within a single proof. The outer elements of a
    proof might be in paragraph form, while the individual cases were presented
    as derivations, or vice versa.

................................................................................
\emph{functional programs} and programming languages; we can state 
equivalences between expressions and
then prove that two programs, or two classes of programs, are equivalent under
those rules. Even more powerfully, if we wish to prove some property of an 
entire language, it is sufficient to show that the equivalences preserve that
property.

Although the additional of equational reasoning to Arend would give the system
a marked increase in logical power, it would also correspondingly increase the
complexity of its implementation and presentation. Equivalence rules require
a different treatment of terms and variables from unification, and it is not
entirely clear how the two will interact, logically. Equivalences over programs
require careful handling of \emph{binders}, language constructs that introduce
new (program) variables into scope. These variables are distinct from the
logic variables, but can both contain, and be contained by, them. Although 
logics exist which provide support for reasoning about binding structures
\mcitep{miller05tocl} their usage in proofs involves additional complexity that
may be at odd with our goal of use in \emph{introductory} curriculum.

\clearpage
\section{Appendix I: Syntax  of the Specification Logic}
\label{sec:spec-syntax}

\newcommand{\nterm}[1]{\mathop{\langle\text{#1}\rangle}}
\newcommand{\sterm}[1]{\mathop{\text{\emph{#1}}}}







|







 







|











|







 







|







 







|
<
|







 







|
>







 







|


|







 







|
>
>
>







 







|







 







|


|







 







|
|

|



|







 







|
>










|
>







 







|







 







|









|







319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
...
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
...
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
...
440
441
442
443
444
445
446
447

448
449
450
451
452
453
454
455
...
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
....
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
....
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
....
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
....
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
....
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
....
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
1932
....
1964
1965
1966
1967
1968
1969
1970
1971
1972
1973
1974
1975
1976
1977
1978
....
2031
2032
2033
2034
2035
2036
2037
2038
2039
2040
2041
2042
2043
2044
2045
2046
2047
2048
2049
2050
2051
2052
2053
2054
2055
    smaller parts, lemmas can be used, like functions, to abstract out 
    commonly-used subproofs, or to break down proofs that would otherwise be
    too large and unwieldy to understand. 

\item The lack of traditional negation eliminates some of the more-confusing 
    elements of traditional logic programming. In particular, Arend has nothing
    corresponding to ``negation as failure''; it is not possible in Arend to 
    know, in a computational sense, when a proposition $P$ fails. Thus, reasoning
    in Arend is entirely about things that are known to be true, never about 
    things that are assumed to be false.
\end{itemize}

Visually, Arend presents proofs as trees of subproofs. A proof in this 
presentation has the form
\[
................................................................................
    will, if sufficiently ``smart'', be able to prove any theorem which a 
    human with near-infinite patience could prove. Proofs produced by automated
    theorem provers are often quite lengthy, some stretching into the 
    thousands-of-pages. Automated theorem provers must often employ 
    sophisticated heuristics in their proof search algorithms, to avoid the
    exponential run times that would otherwise be required.

\item \emph{Model checkers} are concerned the automatic checking of a given 
    model against a formal specification. For example, given a state
    machine as a model of a computational system, we may wish to verify that
    the system never enters some particular set of error states. Since model
    checking is only tangentially related to our subject, we will not discuss
    it further.

\item \emph{Proof assistants} aim to aid in the development and checking of
    formal proofs. While some systems only check proofs for completeness, more
    modern systems will typically also aid the user in the development of a
    proof. Recent examples 
    include Coq \mcitep{Coq:manual}, Twelf \mcitep{pfenning1999system}, and 
    Abella \mcitep{gacek08ijcar}. Several element of Arend's design
    were influenced by Abella, most notably the use of a constructive two-level
    logic for describing and reasoning about systems. For a full history of the 
    development of computer-assisted proof systems, see 
    \mcitet{geuvers2009proof}.

\item More recently, several systems have emerged which try to bridge the gap
    between traditional functional programming and theorem proving. Systems
................................................................................
is the same as saying that $t$ is a proof of $P$. Under this view, proof 
checking is the same as type checking. Arend is not directly based on the
Curry-Howard isomorphism; although its proofs are terms, it does not check them
by computing their types, since terms in Arend are untyped. Nonetheless, we
believe that it should be possible to derive a consistent type system from
Arend's reasoning logic, which would support this interpretation. 

Proof assistants that present a graphical interface are rare. 
While graphical ``wrappers'' exist for some systems (for example, 
ProofWeb\link{http://prover.cs.ru.nl/login.php} for Coq), 
these were not a part of the design of their underlying
systems. The only proof assistant of which we are aware which makes graphical
interaction as much an integral feature as Arend is HLM 
\mcitep{reichelt2010types}. Like Arend, HLM encourages direct manipulation
of in-progress proofs and is explicitly designed with that hope that it will
................................................................................
\begin{itemize}


\item \mcitet{kadoda1999desirable} present the results of a survey on the
    desirable user-interface features in an educational proof assistant. One
    surprising result they describe is a positive correlation between both
    the interactivity of a system, and its ability to work with explicit 
    proof trees, and the ``error-proneness'' of a system. This strikes us as

     surprising, as Arend is both interactive and works with explicit proof trees,
    and yet has virtually no error-proneness during the proof construction
    process, as users are limited strictly to those actions which will
    progress the proof in a valid way.\marginnote{It should be noted
    this author did not discover Kadoda's work until after Arend's design, with
    its emphasis on these features, was largely finalized.}
     However, several features which 
    Kadoda describes as being ``highly'' desirable are present in Arend: its
................................................................................
\subsection{Reasoning logic}

\newthought{Arend's reasoning logic} is closer to a full 
expression of first-order
intuitionistic logic, with extensions to support proofs by single-induction. 
The inference rules defining the reasoning logic are 
presented in Figure \ref{reasoning-rules}. It supports rightward implication 
($\rightarrow$), with the restriction that the left-hand side
 cannot contain nested 
implications, only conjunctions, disjunctions, and atomic 
goals.\footnote{This restriction subsumes the \emph{stratification} 
restriction in Abella; stratification in some form is required to ensure 
monotonicity of the logic.} This implies that antecedents cannot contain
implications, since they cannot be added by $\rightarrow_R$, and are not allowed
in definitions in the specification logic.

................................................................................

\subsection{Proof representation}

Informally, the content of a derivation is relatively simple: a tree of 
\textsc{-Left} and/or \textsc{-Right} rule applications, drawn from the rules
of the reasoning logic in figure \ref{reasoning-rules}. In practice, a more
detailed representation is required, one which, in particular, necessitates the
use of \emph{manual substitution}, rather than the implicit substitution that
would result from naive use of (for example) the system unification in Prolog.

For derivations purely derived from the specification language, manual 
substitution is not required. This is because for any valid derivation of a
proposition expressed in the specification language, the substitution is 
\emph{consistent} throughout the derivation tree; it is not possible for 
different ``branches'' to have different substitutions. (Disjunction may, of
course, result in the generation of multiple distinct derivations, each with its
own unifying substitution, but within any single derivation there is always a
single consistent substitution.)
................................................................................
would need to have a conclusion $X = z \land X = s(x')$, which is already 
inconsistent, and actually impossible to express, because Horn clauses forbid
such conjunctions as conclusions. Conversely, given the conclusion 
$X = z \lor X = s(x')$ we have
the choice of which unification to use, and thus there is no inconsistency.}

Because of this, each branch of a derivation must maintain its own substitution,
applied to its goals as they are expanded. Thus, Arend contains facilities
for implementing its own notion of logical variables, unifying terms containing
these variables (producing a substitution object), and applying substitution
objects to arbitrary terms.

Proofs are represented as a term of the form
\begin{verbatim}
proof(Goal,Ctx,Subst,Proof)
\end{verbatim}
where \texttt{Goal} is the goal to be proved, \texttt{Ctx} is the list of
antecedents (initially empty for most goals), \texttt{Subst} is the 
................................................................................
    various -Left rules of the reasoning logic.
\item \texttt{trivial} --- Proves $\top$.
\item \texttt{hole} --- Proves any goal, but represents an incomplete proof.
\end{itemize}

\subsection{Capture avoidance}

The use of manual substitution means that the proof-checker must also contend
with another troublesome problem which Prolog conceals: avoiding \emph{accidental
capture} when expanding a call to a goal. Consider the goal $\mathsf{nat}(X)$.
We would expect this goal to succeed twice, first with the solution $X = z$. 
However, if we naively unify this goal with the head of the Nat-Succ rule we
get the solution $X = s(X)$ which fails the occurs check. The problem is that
$X$ as present in our goal is not the same variable as $X$ in the Nat-Succ rule.
Variables in rule definitions are \emph{schematic}, their names should be
................................................................................
In this mode it can prove any proposition in the pure specification logic, and
even a few that lie outside it; these extensions include:
\begin{itemize}
\item Simple implications: for example, $P -> P$ can be proved.
\item Proofs involving $\bot$-Left, for example $\bot -> P$. 
\item Proofs involving limited use of other -Left rules. For example, 
    $P \land Q -> P$ can be proved.\footnote{$P \land Q -> P$ produces an 
    infinite sequence of proofs, because the list of antecedents, while properly
    speaking a set, is implemented as a list without duplicate removal, for
    efficiency reasons. Thus it is always possible to case on $P \land Q$, 
    keep the original antecedent, and thus generate an infinite collection of 
    $P$'s, each of which gives, theoretically, a distinct proof.}
\end{itemize}

More interestingly, \texttt{check} can be called with the \emph{goal} unbound
and the proof bound, albeit for a very limited set of proofs. In this mode it
will construct a proposition which is proved by the given proof. 
This behavior is not unexpected; by the Curry-Howard isomorphism proofs are 
................................................................................
\end{lstlisting}

with the (internal) restriction that the IH will never be used without explicit
action on the part of the user. Lemmas, once proved, are represented similarly,
as new program clauses, but requiring explicit use.

A somewhat unfamiliar aspect of Arend's use of induction is how the inductive
hypothesis is applied: ordinarily we would specify those antecedents of the current
proof state which matched the corresponding antecedents of the IH (i.e., 
``apply IH to $nat^\downarrow(X')$''); this would have the effect of introducing
the IH, with the appropriate substitutions, as a new antecedent, where the 
assumption rule could then use it to prove the conclusion.
Purely for user-interface reasons, we
apply the IH by backchaining it against the current \emph{conclusion}, replacing
the goal with the conjunction of the antecedent of the IH (again, with the
appropriate substitutions). The user can then use the $\land$-R rule to 
split the proof into subproofs with atomic goals, each of which can be proved
by the assumption rule.

The inductive hypothesis is used within a proof by backchaining on the current
goal, which must unify with the head of the IH. Recall that backchaining 
replaces the goal with its definition(s). Ordinarily the disjunction of 
................................................................................
\item Currently Arend allows specification authors minimal influence on the
    \emph{user interface}; their power is limited to declaratively describing
    how certain predicates should be rendered as HTML. For more complex
    specifications, this is insufficient. As an example, classical logic can
    be specified in Arend with relative ease, via a predicate \texttt{solve}:
    \texttt{solve(C,G,T)} succeeds if the proposition $G$ evaluates to the
    truth value $T$ in context $C$. However, none of the familiar operations
    for manipulating the consequent and antecedents can be used with this 
    specification,
    as they are ``hidden'' inside the arguments to a predicate. A system 
    allowing specification authors to highlight terms in various contexts as
    targets for user-manipulation would greatly extend the ease-of-use of the
    system when dealing with non-trivial specifications.

\item Many proof assistants allow the user to create \emph{tacticals}, 
    ``shortcuts'' through the proof process or alternate reasoning strategies.
    A cursory glance at the \emph{check/3} predicate at the heart of Arend's
    proof-checking algorithm will reveal a significant amount of similarity
    between the various cases: to apply a -Left or -Right rule, we apply
    some kind of transformation(s) to either one of the antecedents or the 
    consequent,
    and then recursively check zero or more of these transformed subproofs.
    Tacticals allow the user to specify these transformations themselves, in
    a way that enforces their consistency with the underlying logic. For
    some specifications, tacticals could significantly simplify the development
    of otherwise-tedious proofs, by concealing the irrelevant details.

\item In a similar vein, Arend currently requires the user to proceed through
................................................................................
    creating an ecosystem around student-created specifications, proofs, and 
    lemmas, perhaps with collaboration features for multi-student use.

\item Although we believe Arend's derivation-tree presentation of proofs has
    distinct advantages over the traditional paragraph format, there is no
    reason why an alternate user interface could not present proofs in that
    form, allowing users who feel more comfortable with a textual presentation
    to navigate their proofs in that way. Users could easily switch 
    between the two presentations, and any other future presentations that 
    might be added, even in the middle of a proof. Indeed, given the 
    hierarchical structure of proofs, it is entirely possible that the two
    notations could be mixed within a single proof. The outer elements of a
    proof might be in paragraph form, while the individual cases were presented
    as derivations, or vice versa.

................................................................................
\emph{functional programs} and programming languages; we can state 
equivalences between expressions and
then prove that two programs, or two classes of programs, are equivalent under
those rules. Even more powerfully, if we wish to prove some property of an 
entire language, it is sufficient to show that the equivalences preserve that
property.

Although the addition of equational reasoning to Arend would give the system
a marked increase in logical power, it would also correspondingly increase the
complexity of its implementation and presentation. Equivalence rules require
a different treatment of terms and variables from unification, and it is not
entirely clear how the two will interact, logically. Equivalences over programs
require careful handling of \emph{binders}, language constructs that introduce
new (program) variables into scope. These variables are distinct from the
logic variables, but can both contain, and be contained by, them. Although 
logics exist which provide support for reasoning about binding structures
\mcitep{miller05tocl} their usage in proofs involves additional complexity that
may be at odds with our goal of use in \emph{introductory} curriculum.

\clearpage
\section{Appendix I: Syntax  of the Specification Logic}
\label{sec:spec-syntax}

\newcommand{\nterm}[1]{\mathop{\langle\text{#1}\rangle}}
\newcommand{\sterm}[1]{\mathop{\text{\emph{#1}}}}