Check-in [ec0abfb8eb]

Not logged in

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

Overview
Comment:Added reference to Gacek's PhD thesis in the section on induction. Added screenshot of a completed proof.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | bc-subst
Files: files | file ages | folders
SHA1:ec0abfb8ebdfd0b0839df9c266a6b61096ff7800
User & Date: 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
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

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