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 Unified Diffs Show Whitespace Changes Patch

Changes to report/arend-report.bib.

48
49
50
51
52
53
54













55
56
57
58
59
60
61
  author={Page, Rex and Eastlund, Carl and Felleisen, Matthias},
  booktitle={Proceedings of the 2008 international workshop on Functional and declarative programming in education},
  pages={21--30},
  year={2008},
  organization={ACM}
}















@inproceedings{Ford:2004:PEG:964001.964011,
 author = {Ford, Bryan},
 title = {Parsing Expression Grammars: A Recognition-based Syntactic Foundation},
 booktitle = {Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '04},
 year = {2004},







>
>
>
>
>
>
>
>
>
>
>
>
>







48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
  author={Page, Rex and Eastlund, Carl and Felleisen, Matthias},
  booktitle={Proceedings of the 2008 international workshop on Functional and declarative programming in education},
  pages={21--30},
  year={2008},
  organization={ACM}
}


@PHDTHESIS{gacek09phd,
  title = {A Framework for Specifying, Prototyping, and
                  Reasoning about Computational Systems},
  author = {Andrew Gacek},
  school = {University of Minnesota},
  pdf = {http://www.cs.umn.edu/~agacek/pubs/gacek-thesis/gacek-thesis.pdf},
  arxiv = {http://arxiv.org/abs/0910.0747},
  year = 2009,
  month = {September},
  slides = {http://www.cs.umn.edu/~agacek/pubs/slides/gacek09phd-slides.pdf}
}


@inproceedings{Ford:2004:PEG:964001.964011,
 author = {Ford, Bryan},
 title = {Parsing Expression Grammars: A Recognition-based Syntactic Foundation},
 booktitle = {Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '04},
 year = {2004},

Changes to report/arend-report.pdf.

cannot compute difference between binary files

Changes to report/arend-report.tex.

84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
...
987
988
989
990
991
992
993

994
995
996
997












998
999
1000
1001
1002
1003
1004
....
1760
1761
1762
1763
1764
1765
1766
1767


1768
1769
1770
1771
1772
1773
1774
\newcommand{\link}[2]{#2\footnote{\url{#1}}}

% Citations. Both in the text and in the sidebar. The NoHyper makes the actual
% citation link to the bibliography at the end, rather than to the bibentry
% in the margin. It also has the unfortunate side effect of making any URLs
% in the margin entry not work, but the URLs in the actual bibliography still
% work as expected, and they're only a click away.
\newcommand{\mcitet}[1]{\citet{#1}\marginnote{\begin{NoHyper}\bibentry{#1}\end{NoHyper}}}
\newcommand{\mcitep}[1]{\citep{#1}\marginnote{\begin{NoHyper}\bibentry{#1}\end{NoHyper}}}

% Some commands for proof-state objects
\newcommand{\hole}{\;?\;}
\newcommand{\proof}[3]{#2 \vdash #1 \rightarrow #3}
\newcommand{\emptyproof}[1]{\proof{#1}{\Gamma}{\hole{}}}
\newcommand{\ctxproof}[1]{\proof{G}{\Gamma,#1}{\hole{}}}

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

\begin{figure*}[t!]

\begin{centering}
\includegraphics[width=6.5in]{proof-sample.png}
\end{centering}


\caption{The proof assistant interface, with an incomplete inductive proof}
\label{fig:passist1}
\end{figure*}














\clearpage
\section{Implementation}

\newthought{Arend is implemented as} a web-based system, with a server 
component, written in Prolog and running in the 
\link{http://swi-prolog.org}{SWI-Prolog} and a browser-based frontend. 
................................................................................
multiple antecedents is not allowed) and supports only induction global to a 
proof (i.e., nested 
inductions are not allowed, although they can be ``faked'' by using lemmas). 
These restrictions imply that the induction hypothesis can be regarded as
being global to a proof, thus eliminating the need to restrict the scope 
of difference induction hypotheses to different branches of the proof tree.

Internally, induction is implemented by \emph{goal tagging}. When an inductive


proof is declared, a particular goal in the antecedents is selected, by the 
user, to be the target of the induction.\marginnote{For example, in a proof of
$\mathsf{nat}(X) |- \mathsf{add}(X,0,X)$ we would induct on $\mathsf{nat}(X)$.}
This goal must be a user goal; it cannot be a built-in operator such as 
conjunction, disjunction, or unification. The functor of the goal is internally
flagged as being ``big'' (indicated as $\uparrow$) and the induction 
hypothesis is defined in terms of the same goal, but flagged as 







|
|







 







>




>
>
>
>
>
>
>
>
>
>
>
>







 







|
>
>







84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
...
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
....
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
\newcommand{\link}[2]{#2\footnote{\url{#1}}}

% Citations. Both in the text and in the sidebar. The NoHyper makes the actual
% citation link to the bibliography at the end, rather than to the bibentry
% in the margin. It also has the unfortunate side effect of making any URLs
% in the margin entry not work, but the URLs in the actual bibliography still
% work as expected, and they're only a click away.
\newcommand{\mcitet}[2][]{\citet[#1]{#2}\marginnote{\begin{NoHyper}\bibentry{#2}\end{NoHyper}}}
\newcommand{\mcitep}[2][]{\citep[#1]{#2}\marginnote{\begin{NoHyper}\bibentry{#2}\end{NoHyper}}}

% Some commands for proof-state objects
\newcommand{\hole}{\;?\;}
\newcommand{\proof}[3]{#2 \vdash #1 \rightarrow #3}
\newcommand{\emptyproof}[1]{\proof{#1}{\Gamma}{\hole{}}}
\newcommand{\ctxproof}[1]{\proof{G}{\Gamma,#1}{\hole{}}}

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

\begin{figure*}[t!]

\begin{centering}
\includegraphics[width=6.5in]{proof-sample.png}
\end{centering}

\vspace{1em}
\caption{The proof assistant interface, with an incomplete inductive proof}
\label{fig:passist1}
\end{figure*}



\begin{figure*}[t!]

\begin{centering}
\includegraphics[width=6.5in]{proof-complete.png}
\end{centering}

\caption{A completed proof}
\label{fig:passist2}
\end{figure*}


\clearpage
\section{Implementation}

\newthought{Arend is implemented as} a web-based system, with a server 
component, written in Prolog and running in the 
\link{http://swi-prolog.org}{SWI-Prolog} and a browser-based frontend. 
................................................................................
multiple antecedents is not allowed) and supports only induction global to a 
proof (i.e., nested 
inductions are not allowed, although they can be ``faked'' by using lemmas). 
These restrictions imply that the induction hypothesis can be regarded as
being global to a proof, thus eliminating the need to restrict the scope 
of difference induction hypotheses to different branches of the proof tree.

Internally, induction is implemented by 
\emph{goal annotation} \mcitep[sec. 5.2]{gacek09phd}.
When an inductive
proof is declared, a particular goal in the antecedents is selected, by the 
user, to be the target of the induction.\marginnote{For example, in a proof of
$\mathsf{nat}(X) |- \mathsf{add}(X,0,X)$ we would induct on $\mathsf{nat}(X)$.}
This goal must be a user goal; it cannot be a built-in operator such as 
conjunction, disjunction, or unification. The functor of the goal is internally
flagged as being ``big'' (indicated as $\uparrow$) and the induction 
hypothesis is defined in terms of the same goal, but flagged as