From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 28 May 2007 08:38:05 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~6285
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=693e484d94573197108f51e3de4218492d9db3e2;p=helm.git

...
---

diff --git a/helm/www/matita/papers.shtml b/helm/www/matita/papers.shtml
new file mode 100644
index 000000000..9f5bbafaa
--- /dev/null
+++ b/helm/www/matita/papers.shtml
@@ -0,0 +1,168 @@
+<ul>
+  
+  <li class="paper">
+  <span class="paper_author">
+    Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+  </span><br/>
+  <span class="paper_title">
+    The Matita Proof Assistant
+  </span>
+  <a class="paper_download" href="PAPERS/matita.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <a class="paper_download" href="PAPERS/matita.ps">
+    <span class="ps_logo">.ps</span>
+  </a><br/>
+  <span class="paper_info">
+      Submitted to Journal of Automated Reasoning, Special Issue on User
+      Interfaces for Theorem Proving
+  </span><br/>
+  <span class="paper_abstract">
+      Matita is a new document-centric proof assistant that integrates several
+      Mathematical Knowledge Management tools and techniques. In this paper we
+      describe the architecture of Matita and the peculiarities of its user
+      interface.
+  </span>
+  </li>
+  
+  
+  <li class="paper">
+  <span class="paper_author">
+    Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+  </span><br/>
+  <span class="paper_title">
+      Tinycals: step by step tacticals
+  </span>
+  <a class="paper_download" href="PAPERS/tinycals.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <a class="paper_download" href="PAPERS/tinycals.ps">
+    <span class="ps_logo">.ps</span>
+  </a><br/>
+  <span class="paper_info">
+      Submitted to UITP 2006 User Interfaces for Theorem Provers. Seattle, WA
+      -- August 21, 2006.
+  </span><br/>
+  <span class="paper_abstract">
+      Most of the state-of-the-art proof assistants are based on procedural
+      proof languages, scripts, and rely on LCF tacticals as the primary tool
+      for tactics composition. In this paper we discuss how these ingredients
+      do not interact well with user interfaces based on the same interaction
+      paradigm of Proof General (the de facto standard in this field),
+      identifying in the coarse-grainedness of tactical evaluation the key
+      problem.
+
+      We propose tinycals as an alternative to a subset of LCF tacticals,
+      showing that the user does not experience the same problem if tacticals
+      are evaluated in a more fine-grained manner. We present the formal
+      operational semantics of tinycals as well as their implementation in the
+      Matita proof assistant.
+  </span>
+  </li>
+  
+  
+  <li class="paper">
+  <span class="paper_author">Luca Padovani, Stefano Zacchiroli</span><br/>
+  <span class="paper_title">
+      From notation to semantics: there and back again
+  </span>
+  <a class="paper_download" href="PAPERS/notation.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <a class="paper_download" href="PAPERS/notation.ps">
+    <span class="ps_logo">.ps</span>
+  </a><br/>
+  <span class="paper_info">
+      Accepted for publication in the proceedings of MKM 2006: The 5th
+      International Conference on Mathematical Knowledge Management.
+      Wokingham, UK -- August 11-12, 2006.
+  </span><br/>
+  <span class="paper_abstract">
+      Mathematical notation is a structured, open, and ambiguous language.  In
+      order to support mathematical notation in MKM applications one must
+      necessarily take into account presentational as well as semantic aspects.
+      The former are required to create a familiar, comfortable, and usable
+      interface to interact with.  The latter are necessary in order to process
+      the information meaningfully.  In this paper we investigate a framework
+      for dealing with mathematical notation in a meaningful, extensible way,
+      and we show an effective instantiation of its architecture to the field
+      of interactive theorem proving. The framework builds upon well-known
+      concepts and widely-used technologies and it can be easily adopted by
+      other MKM applications.
+  </span>
+  </li>
+  
+  
+  <li class="paper">
+  <span class="paper_author">
+    Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+  </span><br/>
+  <span class="paper_title">
+      A content based mathematical search engine: Whelp
+  </span>
+  <a class="paper_download" href="PAPERS/whelp.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <a class="paper_download" href="PAPERS/whelp.ps">
+    <span class="ps_logo">.ps</span>
+  </a><br/>
+  <span class="paper_info">
+      In Proceedings of TYPES 2004 conference Types for Proofs and Programs.
+      Paris, France -- December 15-18, 2004.  LNCS 3839/2004, Springer-Verlag
+      Heidelberg, ISBN 3-540-31428-8, pp. 17-32
+  </span><br/>
+  <span class="paper_abstract">
+      The prototype of a content based search engine for mathematical knowledge
+      supporting a small set of queries requiring matching and/or typing
+      operations is described. The prototype, called Whelp, exploits a metadata
+      approach for indexing the information that looks far more flexible than
+      traditional indexing techniques for structured expressions like
+      substitution, discrimination, or context trees. The prototype has been
+      instantiated to the standard library of the Coq proof assistant extended
+      with many user contributions.
+  </span>
+  </li>
+  
+  
+  <li class="paper">
+  <span class="paper_author">
+    Claudio Sacerdoti Coen, Stefano Zacchiroli
+  </span><br/>
+  <span class="paper_title">
+    Efficient Ambiguous Parsing of Mathematical Formulae
+  </span>
+  <a class="paper_download" href="PAPERS/disambiguation.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <a class="paper_download" href="PAPERS/disambiguation.ps">
+    <span class="ps_logo">.ps</span>
+  </a><br/>
+  <span class="paper_info">
+      In Proceedings of MKM 2004
+      Third International Conference on Mathematical Knowledge Management.
+      September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
+      Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
+  </span><br/>
+  <span class="paper_abstract">
+      Mathematical notation has the characteristic of being ambiguous:
+      operators can be overloaded and information that can be deduced is often
+      omitted.  Mathematicians are used to this ambiguity and can easily
+      disambiguate a formula making use of the context and of their ability to
+      find the right interpretation.
+
+      Software applications that have to deal with formulae usually avoid these
+      issues by fixing an unambiguous input notation. This solution is annoying
+      for mathematicians because of the resulting tricky syntaxes and becomes a
+      show stopper to the simultaneous adoption of tools characterized by
+      different input languages.
+
+      In this paper we present an efficient algorithm suitable for ambiguous
+      parsing of mathematical formulae. The only requirement of the algorithm
+      is the existence of a validity predicate over abstract syntax trees of
+      incomplete formulae with placeholders. This requirement can be easily
+      fulfilled in the applicative area of interactive proof assistants, and in
+      several other areas of Mathematical Knowledge Management.
+  </span>
+  </li>
+  
+</ul>