helm/www/matita/papers.shtml

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