--- /dev/null
+<papers>
+ <!-- matita {{{ -->
+ <paper name="matita">
+ <authors>
+ <author>Andrea Asperti</author>
+ <author>Claudio Sacerdoti Coen</author>
+ <author>Enrico Tassi</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ The Matita Proof Assistant
+ </title>
+ <abstract>
+ Matita is a new document-centric proof assistant that integrates several
+ Mathematical Knowledge Management tools and techniques. In this paper we
+ describe the architecture of Matita and the peculiarities of its user
+ interface.
+ </abstract>
+ <info>
+ Submitted to <a href="http://www-unix.mcs.anl.gov/JAR/">Journal of
+ Automated Reasoning</a>, Special Issue on User Interfaces for Theorem
+ Proving
+ </info>
+ </paper>
+ <!-- }}} -->
+ <!-- tinycals {{{ -->
+ <paper name="tinycals">
+ <authors>
+ <author>Claudio Sacerdoti Coen</author>
+ <author>Enrico Tassi</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ Tinycals: step by step tacticals
+ </title>
+ <abstract>
+ Most of the state-of-the-art proof assistants are based on procedural
+ proof languages, scripts, and rely on LCF tacticals as the primary tool
+ for tactics composition. In this paper we discuss how these ingredients
+ do not interact well with user interfaces based on the same interaction
+ paradigm of Proof General (the de facto standard in this field),
+ identifying in the coarse-grainedness of tactical evaluation the key
+ problem.
+
+ We propose tinycals as an alternative to a subset of LCF tacticals,
+ showing that the user does not experience the same problem if tacticals
+ are evaluated in a more fine-grained manner. We present the formal
+ operational semantics of tinycals as well as their implementation in the
+ Matita proof assistant.
+ </abstract>
+ <info>
+ Submitted to
+ <a href="http://www.ags.uni-sb.de/~omega/workshops/UITP06/">UITP 2006</a>
+ User Interfaces for Theorem Provers. Seattle, WA -- August 21, 2006.
+ </info>
+ </paper>
+ <!-- }}} -->
+ <!-- notation {{{ -->
+ <paper name="notation">
+ <authors>
+ <author>Luca Padovani</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ From notation to semantics: there and back again
+ </title>
+ <abstract>
+ Mathematical notation is a structured, open, and ambiguous language. In
+ order to support mathematical notation in MKM applications one must
+ necessarily take into account presentational as well as semantic aspects.
+ The former are required to create a familiar, comfortable, and usable
+ interface to interact with. The latter are necessary in order to process
+ the information meaningfully. In this paper we investigate a framework
+ for dealing with mathematical notation in a meaningful, extensible way,
+ and we show an effective instantiation of its architecture to the field
+ of interactive theorem proving. The framework builds upon well-known
+ concepts and widely-used technologies and it can be easily adopted by
+ other MKM applications.
+ </abstract>
+ <info>
+ Accepted for publication in the proceedings of
+ <a href="http://www.reading.ac.uk/MKM06/">MKM 2006</a>: The
+ 5th International Conference on Mathematical Knowledge Management.
+ Wokingham, UK -- August 11-12, 2006.
+ </info>
+ </paper>
+ <!-- }}} -->
+ <!-- whelp {{{ -->
+ <paper name="whelp">
+ <authors>
+ <author>Andrea Asperti</author>
+ <author>Ferruccio Guidi</author>
+ <author>Claudio Sacerdoti Coen</author>
+ <author>Enrico Tassi</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ A content based mathematical search engine: Whelp
+ </title>
+ <abstract>
+ The prototype of a content based search engine for mathematical knowledge
+ supporting a small set of queries requiring matching and/or typing
+ operations is described. The prototype, called Whelp, exploits a metadata
+ approach for indexing the information that looks far more flexible than
+ traditional indexing techniques for structured expressions like
+ substitution, discrimination, or context trees. The prototype has been
+ instantiated to the standard library of the Coq proof assistant extended
+ with many user contributions.
+ </abstract>
+ <info>
+ In Proceedings of
+ <a href="http://types2004.lri.fr/">TYPES 2004 conference</a> Types for
+ Proofs and Programs. Paris, France -- December 15-18, 2004.
+ LNCS 3839/2004, Springer-Verlag Heidelberg, ISBN 3-540-31428-8, pp. 17-32
+ </info>
+ </paper>
+ <!-- }}} -->
+ <!-- disambiguation {{{ -->
+ <paper name="disambiguation">
+ <authors>
+ <author>Claudio Sacerdoti Coen</author>
+ <author>Stefano Zacchiroli</author>
+ </authors>
+ <title>
+ Efficient Ambiguous Parsing of Mathematical Formulae
+ </title>
+ <abstract>
+ Mathematical notation has the characteristic of being ambiguous:
+ operators can be overloaded and information that can be deduced is often
+ omitted. Mathematicians are used to this ambiguity and can easily
+ disambiguate a formula making use of the context and of their ability to
+ find the right interpretation.
+
+ Software applications that have to deal with formulae usually avoid these
+ issues by fixing an unambiguous input notation. This solution is annoying
+ for mathematicians because of the resulting tricky syntaxes and becomes a
+ show stopper to the simultaneous adoption of tools characterized by
+ different input languages.
+
+ In this paper we present an efficient algorithm suitable for ambiguous
+ parsing of mathematical formulae. The only requirement of the algorithm
+ is the existence of a validity predicate over abstract syntax trees of
+ incomplete formulae with placeholders. This requirement can be easily
+ fulfilled in the applicative area of interactive proof assistants, and in
+ several other areas of Mathematical Knowledge Management.
+ </abstract>
+ <info>
+ In Proceedings of <a href="http://mizar.uwb.edu.pl/MKM2004/">MKM 2004</a>
+ Third International Conference on Mathematical Knowledge Management.
+ September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004,
+ Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362
+ </info>
+ </paper>
+ <!-- }}} -->
+</papers>
+<!-- vim:set foldmethod=marker: -->
projects / helm.git / blobdiff