[ Toggle abstracts ]

• Andrea Asperti, Enrico Tassi
  Higher order proof reconstruction from paramodulation-based refutations: the unit equality case .pdf Accepted for publication in the proceedings of MKM 2007: The 6th International Conference on Mathematical Knowledge Management. 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.
• Claudio Sacerdoti Coen, Stefano Zacchiroli
  Spurious Disambiguation Error Detection .pdf Accepted for publication in the proceedings of MKM 2007: The 6th International Conference on Mathematical Knowledge Management. 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.
• Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
  Crafting a Proof Assistant .pdf Accepted for publication in the Proceedings of Types 2006: Conference of the Types Project. Nottingham, UK -- April 18-21, 2006. 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.
• Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
  User Interaction with the Matita Proof Assistant .pdf Accepted for publication in Journal of Automated Reasoning, Special Issue on User Interfaces for Theorem Proving. 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.
• Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
  Tinycals: step by step tacticals .pdf 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 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.
• Luca Padovani, Stefano Zacchiroli
  From notation to semantics: there and back again .pdf Accepted for publication in the proceedings of MKM 2006: The 5th International Conference on Mathematical Knowledge Management. Wokingham, UK -- August 11-12, 2006. 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.
• Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
  A content based mathematical search engine: Whelp .pdf 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 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.
• Claudio Sacerdoti Coen, Stefano Zacchiroli
  Efficient Ambiguous Parsing of Mathematical Formulae .pdf 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 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.