helm/www/matita/papers.shtml

   1 <ul>
   2
   3   <li class="paper">
   4   <span class="paper_author">
   5     Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
   6   </span><br/>
   7   <span class="paper_title">
   8     The Matita Proof Assistant
   9   </span>
  10   <a class="paper_download" href="PAPERS/matita.pdf">
  11     <span class="pdf_logo">.pdf</span>
  12   </a>
  13   <a class="paper_download" href="PAPERS/matita.ps">
  14     <span class="ps_logo">.ps</span>
  15   </a><br/>
  16   <span class="paper_info">
  17       Submitted to Journal of Automated Reasoning, Special Issue on User
  18       Interfaces for Theorem Proving
  19   </span><br/>
  20   <span class="paper_abstract">
  21       Matita is a new document-centric proof assistant that integrates several
  22       Mathematical Knowledge Management tools and techniques. In this paper we
  23       describe the architecture of Matita and the peculiarities of its user
  24       interface.
  25   </span>
  26   </li>
  27
  28
  29   <li class="paper">
  30   <span class="paper_author">
  31     Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
  32   </span><br/>
  33   <span class="paper_title">
  34       Tinycals: step by step tacticals
  35   </span>
  36   <a class="paper_download" href="PAPERS/tinycals.pdf">
  37     <span class="pdf_logo">.pdf</span>
  38   </a>
  39   <a class="paper_download" href="PAPERS/tinycals.ps">
  40     <span class="ps_logo">.ps</span>
  41   </a><br/>
  42   <span class="paper_info">
  43       Submitted to UITP 2006 User Interfaces for Theorem Provers. Seattle, WA
  44       -- August 21, 2006.
  45   </span><br/>
  46   <span class="paper_abstract">
  47       Most of the state-of-the-art proof assistants are based on procedural
  48       proof languages, scripts, and rely on LCF tacticals as the primary tool
  49       for tactics composition. In this paper we discuss how these ingredients
  50       do not interact well with user interfaces based on the same interaction
  51       paradigm of Proof General (the de facto standard in this field),
  52       identifying in the coarse-grainedness of tactical evaluation the key
  53       problem.
  54
  55       We propose tinycals as an alternative to a subset of LCF tacticals,
  56       showing that the user does not experience the same problem if tacticals
  57       are evaluated in a more fine-grained manner. We present the formal
  58       operational semantics of tinycals as well as their implementation in the
  59       Matita proof assistant.
  60   </span>
  61   </li>
  62
  63
  64   <li class="paper">
  65   <span class="paper_author">Luca Padovani, Stefano Zacchiroli</span><br/>
  66   <span class="paper_title">
  67       From notation to semantics: there and back again
  68   </span>
  69   <a class="paper_download" href="PAPERS/notation.pdf">
  70     <span class="pdf_logo">.pdf</span>
  71   </a>
  72   <a class="paper_download" href="PAPERS/notation.ps">
  73     <span class="ps_logo">.ps</span>
  74   </a><br/>
  75   <span class="paper_info">
  76       Accepted for publication in the proceedings of MKM 2006: The 5th
  77       International Conference on Mathematical Knowledge Management.
  78       Wokingham, UK -- August 11-12, 2006.
  79   </span><br/>
  80   <span class="paper_abstract">
  81       Mathematical notation is a structured, open, and ambiguous language.  In
  82       order to support mathematical notation in MKM applications one must
  83       necessarily take into account presentational as well as semantic aspects.
  84       The former are required to create a familiar, comfortable, and usable
  85       interface to interact with.  The latter are necessary in order to process
  86       the information meaningfully.  In this paper we investigate a framework
  87       for dealing with mathematical notation in a meaningful, extensible way,
  88       and we show an effective instantiation of its architecture to the field
  89       of interactive theorem proving. The framework builds upon well-known
  90       concepts and widely-used technologies and it can be easily adopted by
  91       other MKM applications.
  92   </span>
  93   </li>
  94
  95
  96   <li class="paper">
  97   <span class="paper_author">
  98     Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
  99   </span><br/>
 100   <span class="paper_title">
 101       A content based mathematical search engine: Whelp
 102   </span>
 103   <a class="paper_download" href="PAPERS/whelp.pdf">
 104     <span class="pdf_logo">.pdf</span>
 105   </a>
 106   <a class="paper_download" href="PAPERS/whelp.ps">
 107     <span class="ps_logo">.ps</span>
 108   </a><br/>
 109   <span class="paper_info">
 110       In Proceedings of TYPES 2004 conference Types for Proofs and Programs.
 111       Paris, France -- December 15-18, 2004.  LNCS 3839/2004, Springer-Verlag
 112       Heidelberg, ISBN 3-540-31428-8, pp. 17-32
 113   </span><br/>
 114   <span class="paper_abstract">
 115       The prototype of a content based search engine for mathematical knowledge
 116       supporting a small set of queries requiring matching and/or typing
 117       operations is described. The prototype, called Whelp, exploits a metadata
 118       approach for indexing the information that looks far more flexible than
 119       traditional indexing techniques for structured expressions like
 120       substitution, discrimination, or context trees. The prototype has been
 121       instantiated to the standard library of the Coq proof assistant extended
 122       with many user contributions.
 123   </span>
 124   </li>
 125
 126
 127   <li class="paper">
 128   <span class="paper_author">
 129     Claudio Sacerdoti Coen, Stefano Zacchiroli
 130   </span><br/>
 131   <span class="paper_title">
 132     Efficient Ambiguous Parsing of Mathematical Formulae
 133   </span>
 134   <a class="paper_download" href="PAPERS/disambiguation.pdf">
 135     <span class="pdf_logo">.pdf</span>
 136   </a>
 137   <a class="paper_download" href="PAPERS/disambiguation.ps">
 138     <span class="ps_logo">.ps</span>
 139   </a><br/>
 140   <span class="paper_info">
 141       In Proceedings of MKM 2004
 142       Third International Conference on Mathematical Knowledge Management.
 143       September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
 144       Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
 145   </span><br/>
 146   <span class="paper_abstract">
 147       Mathematical notation has the characteristic of being ambiguous:
 148       operators can be overloaded and information that can be deduced is often
 149       omitted.  Mathematicians are used to this ambiguity and can easily
 150       disambiguate a formula making use of the context and of their ability to
 151       find the right interpretation.
 152
 153       Software applications that have to deal with formulae usually avoid these
 154       issues by fixing an unambiguous input notation. This solution is annoying
 155       for mathematicians because of the resulting tricky syntaxes and becomes a
 156       show stopper to the simultaneous adoption of tools characterized by
 157       different input languages.
 158
 159       In this paper we present an efficient algorithm suitable for ambiguous
 160       parsing of mathematical formulae. The only requirement of the algorithm
 161       is the existence of a validity predicate over abstract syntax trees of
 162       incomplete formulae with placeholders. This requirement can be easily
 163       fulfilled in the applicative area of interactive proof assistants, and in
 164       several other areas of Mathematical Knowledge Management.
 165   </span>
 166   </li>
 167
 168 </ul>