+<small>
+ <a style="text-decoration: none;" href="javascript:toggleAbstracts()">[ Toggle abstracts ]</a>
+</small>
+
+<ul>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Enrico Tassi
+ </span><br/>
+ <span class="paper_title">
+ Higher order proof reconstruction from paramodulation-based refutations:
+ the unit equality case
+ </span>
+ <a class="paper_download" href="PAPERS/hopr.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2007: The 6th
+ International Conference on Mathematical Knowledge Management.
+ </span>
+ <span class="paper_abstract">
+ In this paper we address the problem of reconstructing a
+ higher order, checkable proof object starting from a proof trace left by a
+ first order automatic proof searching procedure, in a restricted equational
+ framework. The automatic procedure is based on superposition rules for
+ the unit equality case. Proof transformation techniques aimed to improve
+ the readability of the final proof are discussed.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Claudio Sacerdoti Coen, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Spurious Disambiguation Error Detection
+ </span>
+ <a class="paper_download" href="PAPERS/disambiguation-errors.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2007: The 6th
+ International Conference on Mathematical Knowledge Management.
+ </span>
+ <span class="paper_abstract">
+ The disambiguation approach to the input of formulae enables the user to
+ type correct formulae in a terse syntax close to the usual ambiguous
+ mathematical notation. When it comes to incorrect formulae we want to
+ present only errors related to the interpretation meant by the user, hiding
+ errors related to other interpretations (spurious errors). We propose a
+ heuristic to recognize spurious errors, which has been integrated with our
+ former efficient disambiguation algorithm.
+ </span>
+ </li>
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Crafting a Proof Assistant
+ </span>
+ <a class="paper_download" href="PAPERS/matita_types.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the Proceedings of Types 2006: Conference of
+ the Types Project. Nottingham, UK -- April 18-21, 2006.
+ </span>
+ <span class="paper_abstract">
+ Proof assistants are complex applications whose develop-
+ ment has never been properly systematized or documented. This work is
+ a contribution in this direction, based on our experience with the devel-
+ opment of Matita: a new interactive theorem prover based—as Coq—on
+ the Calculus of Inductive Constructions (CIC). In particular, we analyze
+ its architecture focusing on the dependencies of its components, how they
+ implement the main functionalities, and their degree of reusability.
+ The work is a first attempt to provide a ground for a more direct com-
+ parison between different systems and to highlight the common func-
+ tionalities, not only in view of reusability but also to encourage a more
+ systematic comparison of different softwares and architectural solutions.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ User Interaction with the Matita Proof Assistant
+ </span>
+ <a class="paper_download" href="PAPERS/matita.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in Journal of Automated Reasoning, Special Issue
+ on User Interfaces for Theorem Proving.
+ </span>
+ <span class="paper_abstract">
+ Matita is a new, document-centric, tactic-based interactive theorem
+ prover. This paper focuses on some of the distinctive features of the user interaction
+ with Matita, mostly characterized by the organization of the library as a search-
+ able knowledge base, the emphasis on a high-quality notational rendering, and the
+ complex interplay between syntax, presentation, and semantics.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">
+ Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Tinycals: step by step tacticals
+ </span>
+ <a class="paper_download" href="PAPERS/tinycals.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle,
+ WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 -
+ 142, ISSN:1571-0661
+ </span>
+ <span class="paper_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.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">Luca Padovani, Stefano Zacchiroli</span><br/>
+ <span class="paper_title">
+ From notation to semantics: there and back again
+ </span>
+ <a class="paper_download" href="PAPERS/notation.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ Accepted for publication in the proceedings of MKM 2006: The 5th
+ International Conference on Mathematical Knowledge Management.
+ Wokingham, UK -- August 11-12, 2006.
+ </span>
+ <span class="paper_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.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">
+ Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ A content based mathematical search engine: Whelp
+ </span>
+ <a class="paper_download" href="PAPERS/whelp.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ In Proceedings of TYPES 2004 conference 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
+ </span>
+ <span class="paper_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.
+ </span>
+ </li>
+
+
+ <li class="paper">
+ <span class="paper_author">
+ Claudio Sacerdoti Coen, Stefano Zacchiroli
+ </span><br/>
+ <span class="paper_title">
+ Efficient Ambiguous Parsing of Mathematical Formulae
+ </span>
+ <a class="paper_download" href="PAPERS/disambiguation.pdf">
+ <span class="pdf_logo">.pdf</span>
+ </a>
+ <span class="paper_info">
+ In Proceedings of MKM 2004
+ 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
+ </span>
+ <span class="paper_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.
+ </span>
+ </li>
+
+</ul>