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