X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fpapers.shtml;h=886a87271e47a734652882b4e974812ab41fe16c;hb=2483c02736ae20e93d53333795b668b93a439380;hp=d6f7e029445da54f9567ec58bd4bf5a08a53814f;hpb=3af196f19d0ffa25a294f6f6c1247ac427ad37d1;p=helm.git

diff --git a/helm/www/matita/papers.shtml b/helm/www/matita/papers.shtml
index d6f7e0294..886a87271 100644
--- a/helm/www/matita/papers.shtml
+++ b/helm/www/matita/papers.shtml
@@ -1,3 +1,7 @@
+<small>
+  <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
+</small>
+
 <ul>
   
   <li class="paper">
@@ -12,8 +16,9 @@
     <span class="pdf_logo">.pdf</span>
   </a>
   <span class="paper_info">
-    Accepted for publication in the proceedings of MKM07
-  </span><br/>
+    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
@@ -24,6 +29,31 @@
   </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
@@ -37,7 +67,7 @@
   <span class="paper_info">
     Accepted for publication in the Proceedings of Types 2006: Conference of
     the Types Project. Nottingham, UK -- April 18-21, 2006.
-  </span><br/>
+  </span>
   <span class="paper_abstract">
      Proof assistants are complex applications whose develop-
      ment has never been properly systematized or documented. This work is
@@ -67,7 +97,7 @@
   <span class="paper_info">
     Accepted for publication in Journal of Automated Reasoning, Special Issue
     on User Interfaces for Theorem Proving.
-  </span><br/>
+  </span>
   <span class="paper_abstract">
      Matita is a new, document-centric, tactic-based interactive theorem
      prover. This paper focuses on some of the distinctive features of the user interaction
@@ -92,7 +122,7 @@
     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><br/>
+  </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
@@ -123,7 +153,7 @@
       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
@@ -154,7 +184,7 @@
       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
@@ -183,7 +213,7 @@
       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