Many hyperlinks are disabled.

Use anonymous login
to enable hyperlinks.

Overview

Comment: | Added material to the report on the handling of explicit quantifiers. |
---|---|

Downloads: | Tarball | ZIP archive | SQL archive |

Timelines: | family | ancestors | descendants | both | forall-exists |

Files: | files | file ages | folders |

SHA1: | 8a438a8abdfb67b6d72fac2b284dc0fc06ce5190 |

User & Date: | andy 2015-04-22 10:30:20 |

Context

2015-04-22
| ||

20:49 | Added poster for appreciation reception. check-in: 8078001da1 user: andy tags: trunk | |

10:30 | Added material to the report on the handling of explicit quantifiers. Leaf check-in: 8a438a8abd user: andy tags: forall-exists | |

10:29 | Presentation work. Added PDF of presentation. Leaf check-in: a24ff57f47 user: andy tags: trunk | |

Changes

Changes to report/arend-report.pdf.

cannot compute difference between binary files

Changes to report/arend-report.tex.

1348 1348 is implicitly $\exists$-quantified. 1349 1349 \end{itemize} 1350 1350 1351 1351 Note that, if \texttt{:-} is regarded as $\leftarrow$, this is the opposite of 1352 1352 the implicit quantification in the specification. However, these rules match 1353 1353 the normal expectation for proof-style statements. For example: 1354 1354 \begin{itemize} 1355 -\item $\mathsf{nat}(X) -> \mathsf{add}(X,a,X)$ is equivalent to 1356 - $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,a,X)$. 1355 +\item $\mathsf{nat}(X) -> \mathsf{add}(X,z,X)$ is equivalent to 1356 + $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,z,X)$. 1357 1357 \item $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land 1358 1358 \mathsf{nat}(Z)$ is equivalent to $\forall X,Y: \mathsf{nat}(X) \land 1359 1359 \mathsf{nat}(Y) -> \exists Z: \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$. 1360 1360 \end{itemize} 1361 1361 1362 1362 Internally, when processing a proof tree, Arend maintains two sets of 1363 1363 in-scope variables: \emph{universals} and \emph{existentials}. Universals are ................................................................................ 1424 1424 1425 1425 (This presentation is based in part on that in \mcitet{pfenning2006logic}.) 1426 1426 1427 1427 It is interesting to directly compare the two implementations of unification 1428 1428 (one of the few modules which is semantically similar in both 1429 1429 implementations). Both systems implement the same algorithm. The Javascript 1430 1430 implementation consists of 1431 -136 lines of non-comment code and is quite difficult to follow; the Prolog 1432 -implementation requires only 69 lines, 1433 -an almost 50\% reduction! This despite the fact that the Prolog implementation 1431 +\lnum{136} lines of non-comment code and is quite difficult to follow; the Prolog 1432 +implementation requires only \lnum{69} lines, 1433 +an almost \lnum{50\%} reduction! This despite the fact that the Prolog implementation 1434 1434 does \emph{not} use the built-in unification to simplify the algorithm at all; 1435 1435 it would be largely the same if only traditional assignment were used. 1436 1436 1437 1437 1438 1438 \subsection{Proof Checking} 1439 1439 1440 -The proof checker is implemented in approximately 450 lines of Prolog code. It 1440 +The proof checker is implemented in approximately \lnum{450} lines of Prolog code. It 1441 1441 essentially implements the rules of the reasoning logic presented in figure 1442 1442 \ref{reasoning-rules}, by recursively checking the proof tree. That is, it 1443 1443 first checks the root node to ensure that the proof object is consistent with 1444 1444 the conclusion (antecedents and consequent) by ensuring that it has the correct 1445 1445 number and type of subproofs. The subproofs are then recursively checked, 1446 1446 working through the tree until the axiomatic rules are reached (or, in the 1447 1447 case of an incomplete proof, a \texttt{hole} is found, indicating an unproved ................................................................................ 1879 1879 \] 1880 1880 \[ 1881 1881 \inference[By induction] 1882 1882 {\inference[$->$R] 1883 1883 {\inference[Case] 1884 1884 {\inference[Add-$0$] 1885 1885 {} 1886 - {x = 0 |- \mathsf{add}(0,0,0)} & 1886 + {\mathsf{add}(0,0,0)} & 1887 1887 \inference[Backchain] 1888 1888 {\inference[IH] 1889 - {\assume{x = s(x'), \mathsf{nat}^\downarrow(x') |- \mathsf{nat}^\downarrow(x')}} 1890 - {x = s(x'), \mathsf{nat}^\downarrow(x') |- \mathsf{add}(x',0,x')}} 1891 - {x = s(x'), \mathsf{nat}^\downarrow(x') |- \mathsf{add}(s(x'),0,s(x'))}} 1889 + {\assume{\mathsf{nat}^\downarrow(x') |- \mathsf{nat}^\downarrow(x')}} 1890 + {\mathsf{nat}^\downarrow(x') |- \mathsf{add}(x',0,x')}} 1891 + {\mathsf{nat}^\downarrow(x') |- \mathsf{add}(s(x'),0,s(x'))}} 1892 1892 {\mathsf{nat}^\uparrow(x) |- \mathsf{add}(x,0,x)}} 1893 1893 {\mathsf{nat}^\uparrow(x) -> \mathsf{add}(x,0,x)}} 1894 1894 {\mathsf{nat}(x) -> \mathsf{add}(x,0,x)} 1895 1895 \] 1896 1896 (This example also demonstrates one of the flaws of the derivation proof format, 1897 1897 its insatiable appetite for horizontal space.) 1898 1898