helm/www/matita1.0/xml/papers.xml

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