From: Stefano Zacchiroli Date: Thu, 10 Nov 2005 15:22:13 +0000 (+0000) Subject: paper skeleton X-Git-Tag: V_0_7_2_3~93 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=52f3181ce6b17977eaf30007ad44bcaa25db4519;p=helm.git paper skeleton --- diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index d6dae46e7..d08175719 100644 --- a/helm/papers/matita/matita.tex +++ b/helm/papers/matita/matita.tex @@ -5,31 +5,34 @@ \usepackage{hyperref} \usepackage{picins} -\newcommand{\whelp}{Whelp} - %\newcommand{\logo}[3]{ %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}} %} -\newcommand{\coq}{Coq} -\newcommand{\mowgli}{MoWGLI} -\newcommand{\IR}{\ensuremath{\mathbb{R}}} +\newcommand{\AUTO}{\textsc{Auto}} +\newcommand{\COQ}{Coq} +\newcommand{\ELIM}{\textsc{Elim}} +\newcommand{\HELM}{Helm} +\newcommand{\HINT}{\textsc{Hint}} \newcommand{\IN}{\ensuremath{\mathbb{N}}} -\newcommand{\instance}{\textsc{Instance}} -\newcommand{\auto}{\textsc{Auto}} -\newcommand{\hint}{\textsc{Hint}} -\newcommand{\locate}{\textsc{Locate}} -\newcommand{\elim}{\textsc{Elim}} -\newcommand{\match}{\textsc{Match}} -\newcommand{\texmacro}[1]{\texttt{\char92 #1}} -\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}} -\newcommand{\NAT}{\ensuremath{\mathit{nat}}} -\newcommand{\Prop}{\mathit{Prop}} -\newcommand{\natind}{\mathit{nat\_ind}} -\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline} +\newcommand{\INSTANCE}{\textsc{Instance}} +\newcommand{\IR}{\ensuremath{\mathbb{R}}} \newcommand{\LIBXSLT}{LibXSLT} +\newcommand{\LOCATE}{\textsc{Locate}} +\newcommand{\MATCH}{\textsc{Match}} +\newcommand{\MATITA}{Matita} +\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline} +\newcommand{\MOWGLI}{MoWGLI} +\newcommand{\NAT}{\ensuremath{\mathit{nat}}} +\newcommand{\NATIND}{\mathit{nat\_ind}} \newcommand{\OCAML}{OCaml} +\newcommand{\PROP}{\mathit{Prop}} +\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}} +\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}} \newcommand{\UWOBO}{UWOBO} +\newcommand{\WHELP}{Whelp} + +\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1} \title{The proof assistant Matita} \author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi @@ -47,13 +50,81 @@ \section{Introduction} \label{sec:intro} -{\bf Acknowledgements} +\begin{itemize} + \item scelta del sistema fondazionale + \item sistema indipendente (da Coq) + \begin{itemize} + \item possibilit\`a di sperimentare (soluzioni architetturali, logiche, + implementative, \dots) + \item compatibilit\`a con sistemi legacy + \end{itemize} +\end{itemize} + +\textbf{Acknowledgements} We would like to thank all the students that during the past -five years collaborated in the Helm project and contributed to +five years collaborated in the \HELM{} project and contributed to the development of Matita, and in particular A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi, V.Tamburrelli. +\section{Features} + +\subsection{mathml} +\ASSIGNEDTO{zack} + +\subsection{metavariabili} +\ASSIGNEDTO{csc} + +\subsection{pattern} +\ASSIGNEDTO{gares} + +\subsection{tatticali} +\ASSIGNEDTO{gares} + +\subsection{disambiguazione} +\ASSIGNEDTO{zack} + +\subsection{notazione} +\ASSIGNEDTO{zack} + +\subsection{libreria tutta visibile} +\ASSIGNEDTO{csc} + +\subsection{ricerca e indicizzazione} +\ASSIGNEDTO{andrea} + +\subsection{auto} +\ASSIGNEDTO{andrea} + +\subsection{xml / gestione della libreria} +\ASSIGNEDTO{gares} + +\subsection{named variable} +\ASSIGNEDTO{csc} + +\subsection{assenza di proof tree / resa in linguaggio naturale} +\ASSIGNEDTO{andrea} + +\subsection{selezione semantica, cut paste, hyperlink} +\ASSIGNEDTO{zack} + +\subsection{sostituzioni esplicite vs moduli} +\ASSIGNEDTO{csc} + +\section{Drawbacks, missing, \dots} + +\subsection{moduli} +\ASSIGNEDTO{} + +\subsection{ltac} +\ASSIGNEDTO{} + +\subsection{estrazione} +\ASSIGNEDTO{} + +\subsection{localizzazione errori} +\ASSIGNEDTO{} + \begin{thebibliography}{} \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen,