helm/www/matita/papers.shtml

   1 <script type="text/javascript">
   2   function toggleAbstracts() {
   3     abstracts = document.getElementsByTagName("span");
   4     len = abstracts.length;
   5     for (i=0; i != len-1; i++) {
   6       elt = abstracts.item(i);
   7       if (elt.hasAttribute("class")) {
   8         if (elt.getAttribute("class") == "paper_abstract") {
   9           if (elt.style.display != "none") {
  10             elt.style.display = "none";
  11           } else {
  12             elt.style.display = "inline";
  13           }
  14         }
  15       }
  16     }
  17   }
  18 </script>
  19 <small>
  20   <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
  21 </small>
  22
  23 <ul>
  24
  25   <li class="paper">
  26   <span class="paper_author">
  27     Andrea Asperti, Enrico Tassi
  28   </span><br/>
  29   <span class="paper_title">
  30     Higher order proof reconstruction from paramodulation-based refutations:
  31     the unit equality case
  32   </span>
  33   <a class="paper_download" href="PAPERS/hopr.pdf">
  34     <span class="pdf_logo">.pdf</span>
  35   </a>
  36   <span class="paper_info">
  37     Accepted for publication in the proceedings of MKM 2007: The 6th
  38     International Conference on Mathematical Knowledge Management.
  39   </span>
  40   <span class="paper_abstract">
  41     In this paper we address the problem of reconstructing a
  42     higher order, checkable proof object starting from a proof trace left by a
  43     first order automatic proof searching procedure, in a restricted equational
  44     framework. The automatic procedure is based on superposition rules for
  45     the unit equality case. Proof transformation techniques aimed to improve
  46     the readability of the final proof are discussed.
  47   </span>
  48   </li>
  49
  50   <li class="paper">
  51   <span class="paper_author">
  52     Claudio Sacerdoti Coen, Stefano Zacchiroli
  53   </span><br/>
  54   <span class="paper_title">
  55     Spurious Disambiguation Error Detection
  56   </span>
  57   <a class="paper_download" href="PAPERS/disambiguation-errors.pdf">
  58     <span class="pdf_logo">.pdf</span>
  59   </a>
  60   <span class="paper_info">
  61     Accepted for publication in the proceedings of MKM 2007: The 6th
  62     International Conference on Mathematical Knowledge Management.
  63   </span>
  64   <span class="paper_abstract">
  65     The disambiguation approach to the input of formulae enables the user to
  66     type correct formulae in a terse syntax close to the usual ambiguous
  67     mathematical notation. When it comes to incorrect formulae we want to
  68     present only errors related to the interpretation meant by the user, hiding
  69     errors related to other interpretations (spurious errors). We propose a
  70     heuristic to recognize spurious errors, which has been integrated with our
  71     former efficient disambiguation algorithm.
  72   </span>
  73   </li>
  74
  75   <li class="paper">
  76   <span class="paper_author">
  77     Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
  78   </span><br/>
  79   <span class="paper_title">
  80     Crafting a Proof Assistant
  81   </span>
  82   <a class="paper_download" href="PAPERS/matita_types.pdf">
  83     <span class="pdf_logo">.pdf</span>
  84   </a>
  85   <span class="paper_info">
  86     Accepted for publication in the Proceedings of Types 2006: Conference of
  87     the Types Project. Nottingham, UK -- April 18-21, 2006.
  88   </span>
  89   <span class="paper_abstract">
  90      Proof assistants are complex applications whose develop-
  91      ment has never been properly systematized or documented. This work is
  92      a contribution in this direction, based on our experience with the devel-
  93      opment of Matita: a new interactive theorem prover based—as Coq—on
  94      the Calculus of Inductive Constructions (CIC). In particular, we analyze
  95      its architecture focusing on the dependencies of its components, how they
  96      implement the main functionalities, and their degree of reusability.
  97      The work is a first attempt to provide a ground for a more direct com-
  98      parison between different systems and to highlight the common func-
  99      tionalities, not only in view of reusability but also to encourage a more
 100      systematic comparison of different softwares and architectural solutions.
 101   </span>
 102   </li>
 103
 104
 105   <li class="paper">
 106   <span class="paper_author">
 107     Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
 108   </span><br/>
 109   <span class="paper_title">
 110     User Interaction with the Matita Proof Assistant
 111   </span>
 112   <a class="paper_download" href="PAPERS/matita.pdf">
 113     <span class="pdf_logo">.pdf</span>
 114   </a>
 115   <span class="paper_info">
 116     Accepted for publication in Journal of Automated Reasoning, Special Issue
 117     on User Interfaces for Theorem Proving.
 118   </span>
 119   <span class="paper_abstract">
 120      Matita is a new, document-centric, tactic-based interactive theorem
 121      prover. This paper focuses on some of the distinctive features of the user interaction
 122      with Matita, mostly characterized by the organization of the library as a search-
 123      able knowledge base, the emphasis on a high-quality notational rendering, and the
 124      complex interplay between syntax, presentation, and semantics.
 125   </span>
 126   </li>
 127
 128
 129   <li class="paper">
 130   <span class="paper_author">
 131     Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
 132   </span><br/>
 133   <span class="paper_title">
 134       Tinycals: step by step tacticals
 135   </span>
 136   <a class="paper_download" href="PAPERS/tinycals.pdf">
 137     <span class="pdf_logo">.pdf</span>
 138   </a>
 139   <span class="paper_info">
 140     In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle,
 141     WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 -
 142     142, ISSN:1571-0661
 143   </span>
 144   <span class="paper_abstract">
 145       Most of the state-of-the-art proof assistants are based on procedural
 146       proof languages, scripts, and rely on LCF tacticals as the primary tool
 147       for tactics composition. In this paper we discuss how these ingredients
 148       do not interact well with user interfaces based on the same interaction
 149       paradigm of Proof General (the de facto standard in this field),
 150       identifying in the coarse-grainedness of tactical evaluation the key
 151       problem.
 152
 153       We propose tinycals as an alternative to a subset of LCF tacticals,
 154       showing that the user does not experience the same problem if tacticals
 155       are evaluated in a more fine-grained manner. We present the formal
 156       operational semantics of tinycals as well as their implementation in the
 157       Matita proof assistant.
 158   </span>
 159   </li>
 160
 161
 162   <li class="paper">
 163   <span class="paper_author">Luca Padovani, Stefano Zacchiroli</span><br/>
 164   <span class="paper_title">
 165       From notation to semantics: there and back again
 166   </span>
 167   <a class="paper_download" href="PAPERS/notation.pdf">
 168     <span class="pdf_logo">.pdf</span>
 169   </a>
 170   <span class="paper_info">
 171       Accepted for publication in the proceedings of MKM 2006: The 5th
 172       International Conference on Mathematical Knowledge Management.
 173       Wokingham, UK -- August 11-12, 2006.
 174   </span>
 175   <span class="paper_abstract">
 176       Mathematical notation is a structured, open, and ambiguous language.  In
 177       order to support mathematical notation in MKM applications one must
 178       necessarily take into account presentational as well as semantic aspects.
 179       The former are required to create a familiar, comfortable, and usable
 180       interface to interact with.  The latter are necessary in order to process
 181       the information meaningfully.  In this paper we investigate a framework
 182       for dealing with mathematical notation in a meaningful, extensible way,
 183       and we show an effective instantiation of its architecture to the field
 184       of interactive theorem proving. The framework builds upon well-known
 185       concepts and widely-used technologies and it can be easily adopted by
 186       other MKM applications.
 187   </span>
 188   </li>
 189
 190
 191   <li class="paper">
 192   <span class="paper_author">
 193     Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
 194   </span><br/>
 195   <span class="paper_title">
 196       A content based mathematical search engine: Whelp
 197   </span>
 198   <a class="paper_download" href="PAPERS/whelp.pdf">
 199     <span class="pdf_logo">.pdf</span>
 200   </a>
 201   <span class="paper_info">
 202       In Proceedings of TYPES 2004 conference Types for Proofs and Programs.
 203       Paris, France -- December 15-18, 2004.  LNCS 3839/2004, Springer-Verlag
 204       Heidelberg, ISBN 3-540-31428-8, pp. 17-32
 205   </span>
 206   <span class="paper_abstract">
 207       The prototype of a content based search engine for mathematical knowledge
 208       supporting a small set of queries requiring matching and/or typing
 209       operations is described. The prototype, called Whelp, exploits a metadata
 210       approach for indexing the information that looks far more flexible than
 211       traditional indexing techniques for structured expressions like
 212       substitution, discrimination, or context trees. The prototype has been
 213       instantiated to the standard library of the Coq proof assistant extended
 214       with many user contributions.
 215   </span>
 216   </li>
 217
 218
 219   <li class="paper">
 220   <span class="paper_author">
 221     Claudio Sacerdoti Coen, Stefano Zacchiroli
 222   </span><br/>
 223   <span class="paper_title">
 224     Efficient Ambiguous Parsing of Mathematical Formulae
 225   </span>
 226   <a class="paper_download" href="PAPERS/disambiguation.pdf">
 227     <span class="pdf_logo">.pdf</span>
 228   </a>
 229   <span class="paper_info">
 230       In Proceedings of MKM 2004
 231       Third International Conference on Mathematical Knowledge Management.
 232       September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
 233       Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
 234   </span>
 235   <span class="paper_abstract">
 236       Mathematical notation has the characteristic of being ambiguous:
 237       operators can be overloaded and information that can be deduced is often
 238       omitted.  Mathematicians are used to this ambiguity and can easily
 239       disambiguate a formula making use of the context and of their ability to
 240       find the right interpretation.
 241
 242       Software applications that have to deal with formulae usually avoid these
 243       issues by fixing an unambiguous input notation. This solution is annoying
 244       for mathematicians because of the resulting tricky syntaxes and becomes a
 245       show stopper to the simultaneous adoption of tools characterized by
 246       different input languages.
 247
 248       In this paper we present an efficient algorithm suitable for ambiguous
 249       parsing of mathematical formulae. The only requirement of the algorithm
 250       is the existence of a validity predicate over abstract syntax trees of
 251       incomplete formulae with placeholders. This requirement can be easily
 252       fulfilled in the applicative area of interactive proof assistants, and in
 253       several other areas of Mathematical Knowledge Management.
 254   </span>
 255   </li>
 256
 257 </ul>