X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fpapers.shtml;h=2e67afd9aa42584a36860ed046c6dcaf00b71660;hb=7c1364138afcea82e7928dbb88054d6e33478687;hp=9f5bbafaa563660c09a54a161d58c94a8284e88d;hpb=693e484d94573197108f51e3de4218492d9db3e2;p=helm.git

diff --git a/helm/www/matita/papers.shtml b/helm/www/matita/papers.shtml
index 9f5bbafaa..2e67afd9a 100644
--- a/helm/www/matita/papers.shtml
+++ b/helm/www/matita/papers.shtml
@@ -1,27 +1,127 @@
+<script type="text/javascript">
+  function toggleAbstracts() {
+    abstracts = document.getElementsByTagName("span");
+    len = abstracts.length;
+    for (i=0; i != len-1; i++) {
+      elt = abstracts.item(i);
+      if (elt.hasAttribute("class")) {
+	if (elt.getAttribute("class") == "paper_abstract") {
+	  if (elt.style.display != "none") {
+	    elt.style.display = "none";
+	  } else {
+	    elt.style.display = "inline";
+	  }
+	}
+      }
+    }
+  }
+</script>
+<small>
+  <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
+</small>
+
 <ul>
   
+  <li class="paper">
+  <span class="paper_author">
+    Andrea Asperti, Enrico Tassi
+  </span><br/>
+  <span class="paper_title">
+    Higher order proof reconstruction from paramodulation-based refutations:
+    the unit equality case
+  </span>
+  <a class="paper_download" href="PAPERS/hopr.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <span class="paper_info">
+    Accepted for publication in the proceedings of MKM 2007: The 6th
+    International Conference on Mathematical Knowledge Management.
+  </span>
+  <span class="paper_abstract">
+    In this paper we address the problem of reconstructing a
+    higher order, checkable proof object starting from a proof trace left by a
+    first order automatic proof searching procedure, in a restricted equational
+    framework. The automatic procedure is based on superposition rules for
+    the unit equality case. Proof transformation techniques aimed to improve
+    the readability of the final proof are discussed.
+  </span>
+  </li>
+  
+  <li class="paper">
+  <span class="paper_author">
+    Claudio Sacerdoti Coen, Stefano Zacchiroli
+  </span><br/>
+  <span class="paper_title">
+    Spurious Disambiguation Error Detection
+  </span>
+  <a class="paper_download" href="PAPERS/disambiguation-errors.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <span class="paper_info">
+    Accepted for publication in the proceedings of MKM 2007: The 6th
+    International Conference on Mathematical Knowledge Management.
+  </span>
+  <span class="paper_abstract">
+    The disambiguation approach to the input of formulae enables the user to
+    type correct formulae in a terse syntax close to the usual ambiguous
+    mathematical notation. When it comes to incorrect formulae we want to
+    present only errors related to the interpretation meant by the user, hiding
+    errors related to other interpretations (spurious errors). We propose a
+    heuristic to recognize spurious errors, which has been integrated with our
+    former efficient disambiguation algorithm.
+  </span>
+  </li>
+  
   <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
+    Crafting a Proof Assistant
   </span>
-  <a class="paper_download" href="PAPERS/matita.pdf">
+  <a class="paper_download" href="PAPERS/matita_types.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
+    Accepted for publication in the Proceedings of Types 2006: Conference of
+    the Types Project. Nottingham, UK -- April 18-21, 2006.
+  </span>
+  <span class="paper_abstract">
+     Proof assistants are complex applications whose develop-
+     ment has never been properly systematized or documented. This work is
+     a contribution in this direction, based on our experience with the devel-
+     opment of Matita: a new interactive theorem prover based—as Coq—on
+     the Calculus of Inductive Constructions (CIC). In particular, we analyze
+     its architecture focusing on the dependencies of its components, how they
+     implement the main functionalities, and their degree of reusability.
+     The work is a first attempt to provide a ground for a more direct com-
+     parison between different systems and to highlight the common func-
+     tionalities, not only in view of reusability but also to encourage a more
+     systematic comparison of different softwares and architectural solutions.
+  </span>
+  </li>
+  
+  
+  <li class="paper">
+  <span class="paper_author">
+    Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
   </span><br/>
+  <span class="paper_title">
+    User Interaction with the Matita Proof Assistant
+  </span>
+  <a class="paper_download" href="PAPERS/matita.pdf">
+    <span class="pdf_logo">.pdf</span>
+  </a>
+  <span class="paper_info">
+    Accepted for publication in Journal of Automated Reasoning, Special Issue
+    on User Interfaces for Theorem Proving.
+  </span>
   <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.
+     Matita is a new, document-centric, tactic-based interactive theorem
+     prover. This paper focuses on some of the distinctive features of the user interaction
+     with Matita, mostly characterized by the organization of the library as a search-
+     able knowledge base, the emphasis on a high-quality notational rendering, and the
+     complex interplay between syntax, presentation, and semantics.
   </span>
   </li>
   
@@ -36,13 +136,11 @@
   <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/>
+    In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle,
+    WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 -
+    142, ISSN:1571-0661
+  </span>
   <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
@@ -69,14 +167,11 @@
   <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>
   <span class="paper_abstract">
       Mathematical notation is a structured, open, and ambiguous language.  In
       order to support mathematical notation in MKM applications one must
@@ -103,14 +198,11 @@
   <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>
   <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
@@ -134,15 +226,12 @@
   <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>
   <span class="paper_abstract">
       Mathematical notation has the characteristic of being ambiguous:
       operators can be overloaded and information that can be deduced is often