and Enrico Tassi and Stefano Zacchiroli",
title = "A content based mathematical search engine: Whelp",
booktitle = "Post-proceedings of the Types 2004 International Conference",
- volume = "LNCS, (to appear)",
- pages = "xxx--xxx",
+ volume = "LNCS, 3839",
+ pages = "17--32",
publisher = "Springer-Verlag",
year = "2004"
}
@misc{CoqManual,
title = "The {C}oq Proof Assistant Reference Manual",
- author = "The Coq Development Team",
+ author = "{The Coq Development Team}",
howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
year = {2005},
key = "CoqManual"
howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
year = {2003},
url = "\url{http://www.w3.org/TR/MathML2}",
- key = "Mathematical"
+ key = "MathML"
}
@misc{xml,
howpublished = "W3C Recommendation 10 February 1998,
\url{http://www.w3.org/TR/REC-xml}",
url = "\url{http://www.w3.org/TR/REC-xml}",
- key = "Extensible"
+ key = "XML"
}
@misc{dom,
Asperti, A., F. Guidi, C. {Sacerdoti Coen}, E. Tassi, and S. Zacchiroli: 2004,
`A content based mathematical search engine: Whelp'.
\newblock In: {\em Post-proceedings of the Types 2004 International
- Conference}, Vol. LNCS, (to appear). pp. xxx--xxx.
+ Conference}, Vol. LNCS, 3839. pp. 17--32.
\bibitem{content-centric}
Asperti, A., L. padovani, C. {Sacerdoti Coen}, and irene Schena: 2000,
Informatique et en Automatique), France.
\bibitem{mathml}
-Mathematical: 2003, `Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion
- 2.0'.
+MathML: 2003, `Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0'.
\newblock W3C Recommendation 21 February 2001,
\url{http://www.w3.org/TR/MathML2}.
of Mathematical Knowledge Management 2004}, Vol. LNCS, 3119. pp. 347--362.
\bibitem{CoqManual}
-Team, T. C.~D.: 2005, `The {C}oq Proof Assistant Reference Manual'.
+{The Coq Development Team}: 2005, `The {C}oq Proof Assistant Reference Manual'.
\newblock \\\url{http://coq.inria.fr/doc/main.html}.
\bibitem{Werner}
%theorem valid_name: \forall n,m. m + n = n \to m = O.
% intros (n m H).
%\end{grafite}
-%\noindent
+
Consider the following sequent
\sequent{
n:nat\\
H: m + n = n}{
m=O
}
-\noindent
+
To change the right part of the equivalence of the $H$
hypothesis with $O + n$ the user selects and pastes it as the pattern
in the following statement.
\begin{grafite}
change in H:(? ? ? %) with (O + n).
\end{grafite}
-\noindent
+
To understand the pattern (or produce it by hand) the user should be
aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
that the pattern selects only the third argument of $eq$.
\begin{grafite}
change in H match n with (O + n).
\end{grafite}
-\noindent
+
In this case the $\NT{sequent\_path}$ selects the whole $H$, while
the second phase locates $n$.
\begin{grafite}
change in H:(? ? (? ? %) %) with (O + n).
\end{grafite}
-\noindent
\subsubsection{Tactics supporting patterns}