Check-in [ec0abfb8eb]

Not logged in

Overview
Comment: Added reference to Gacek's PhD thesis in the section on induction. Added screenshot of a completed proof. Tarball | ZIP archive | SQL archive family | ancestors | descendants | both | bc-subst files | file ages | folders ec0abfb8ebdfd0b0839df9c266a6b61096ff7800 andy 2015-04-21 16:26:30
Context
 2015-04-21 19:26 The new clausal-expansion system for goals is complete. Closed-Leaf check-in: d8a8e82a90 user: andy tags: bc-subst 16:26 Added reference to Gacek's PhD thesis in the section on induction. Added screenshot of a completed proof. check-in: ec0abfb8eb user: andy tags: bc-subst 16:25 Removed hover styles from premise/conclusion classes (this should be handled in JS, so that it can be disabled when the proof is complete). check-in: 6feebbe110 user: andy tags: bc-subst
Changes

Changes to report/arend-report.bib.

    48     48     author={Page, Rex and Eastlund, Carl and Felleisen, Matthias},
49     49     booktitle={Proceedings of the 2008 international workshop on Functional and declarative programming in education},
50     50     pages={21--30},
51     51     year={2008},
52     52     organization={ACM}
53     53   }
54     54
55  +
56  +@PHDTHESIS{gacek09phd,
57  +  title = {A Framework for Specifying, Prototyping, and
58  +                  Reasoning about Computational Systems},
59  +  author = {Andrew Gacek},
60  +  school = {University of Minnesota},
61  +  pdf = {http://www.cs.umn.edu/~agacek/pubs/gacek-thesis/gacek-thesis.pdf},
62  +  arxiv = {http://arxiv.org/abs/0910.0747},
63  +  year = 2009,
64  +  month = {September},
65  +  slides = {http://www.cs.umn.edu/~agacek/pubs/slides/gacek09phd-slides.pdf}
66  +}
67  +
55     68
56     69   @inproceedings{Ford:2004:PEG:964001.964011,
57     70    author = {Ford, Bryan},
58     71    title = {Parsing Expression Grammars: A Recognition-based Syntactic Foundation},
59     72    booktitle = {Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
60     73    series = {POPL '04},
61     74    year = {2004},



Changes to report/arend-report.pdf.

cannot compute difference between binary files



Changes to report/arend-report.tex.

    84     84   \newcommand{\link}[2]{#2\footnote{\url{#1}}}
85     85
86     86   % Citations. Both in the text and in the sidebar. The NoHyper makes the actual
87     87   % citation link to the bibliography at the end, rather than to the bibentry
88     88   % in the margin. It also has the unfortunate side effect of making any URLs
89     89   % in the margin entry not work, but the URLs in the actual bibliography still
90     90   % work as expected, and they're only a click away.
91         -\newcommand{\mcitet}[1]{\citet{#1}\marginnote{\begin{NoHyper}\bibentry{#1}\end{NoHyper}}}
92         -\newcommand{\mcitep}[1]{\citep{#1}\marginnote{\begin{NoHyper}\bibentry{#1}\end{NoHyper}}}
91  +\newcommand{\mcitet}[2][]{\citet[#1]{#2}\marginnote{\begin{NoHyper}\bibentry{#2}\end{NoHyper}}}
92  +\newcommand{\mcitep}[2][]{\citep[#1]{#2}\marginnote{\begin{NoHyper}\bibentry{#2}\end{NoHyper}}}
93     93
94     94   % Some commands for proof-state objects
95     95   \newcommand{\hole}{\;?\;}
96     96   \newcommand{\proof}[3]{#2 \vdash #1 \rightarrow #3}
97     97   \newcommand{\emptyproof}[1]{\proof{#1}{\Gamma}{\hole{}}}
98     98   \newcommand{\ctxproof}[1]{\proof{G}{\Gamma,#1}{\hole{}}}
99     99
................................................................................
987    987
988    988   \begin{figure*}[t!]
989    989
990    990   \begin{centering}
991    991   \includegraphics[width=6.5in]{proof-sample.png}
992    992   \end{centering}
993    993
994  +\vspace{1em}
994    995   \caption{The proof assistant interface, with an incomplete inductive proof}
995    996   \label{fig:passist1}
996    997   \end{figure*}
997    998
999  +
1000  +
1001  +\begin{figure*}[t!]
1002  +
1003  +\begin{centering}
1004  +\includegraphics[width=6.5in]{proof-complete.png}
1005  +\end{centering}
1006  +
1007  +\caption{A completed proof}
1008  +\label{fig:passist2}
1009  +\end{figure*}
1010  +
998   1011
999   1012   \clearpage
1000   1013   \section{Implementation}
1001   1014
1002   1015   \newthought{Arend is implemented as} a web-based system, with a server
1003   1016   component, written in Prolog and running in the
1004   1017   \link{http://swi-prolog.org}{SWI-Prolog} and a browser-based frontend.
................................................................................
1760   1773   multiple antecedents is not allowed) and supports only induction global to a
1761   1774   proof (i.e., nested
1762   1775   inductions are not allowed, although they can be faked'' by using lemmas).
1763   1776   These restrictions imply that the induction hypothesis can be regarded as
1764   1777   being global to a proof, thus eliminating the need to restrict the scope
1765   1778   of difference induction hypotheses to different branches of the proof tree.
1766   1779
1767         -Internally, induction is implemented by \emph{goal tagging}. When an inductive
1780  +Internally, induction is implemented by
1781  +\emph{goal annotation} \mcitep[sec. 5.2]{gacek09phd}.
1782  +When an inductive
1768   1783   proof is declared, a particular goal in the antecedents is selected, by the
1769   1784   user, to be the target of the induction.\marginnote{For example, in a proof of
1770   1785   $\mathsf{nat}(X) |- \mathsf{add}(X,0,X)$ we would induct on $\mathsf{nat}(X)$.}
1771   1786   This goal must be a user goal; it cannot be a built-in operator such as
1772   1787   conjunction, disjunction, or unification. The functor of the goal is internally
1773   1788   flagged as being big'' (indicated as $\uparrow$) and the induction
1774   1789   hypothesis is defined in terms of the same goal, but flagged as