helm/www/matita/papers.shtml

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