Abstract
Matita is a proof assistant characterised by a rich, user extensible, output facility based on a widget for the rendering of MathML Presentation, and by the automatic handling of overloading by means of a flexible disambiguation mechanism. We show how to use these features to obtain a simple learning environment for natural deduction, without modifying the source code or Matita.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Adams, A.A.: Digitisation, representation and formalisation: Digital libraries of mathematics. In: Davenport, J.H., Asperti, A., Buchberger, B. (eds.) MKM 2003. LNCS, vol. 2594, pp. 1–16. Springer, Heidelberg (2003)
The Matita interactive theorem prover, http://matita.cs.unibo.it
Padovani, L.: A math canvas for the GNOME desktop. In: 5th Annual GNOME User and Developer European Conference (GUADEC 2004), vol. 107. Agder University College (2004)
Padovani, L., Zacchiroli, S.: From notation to semantics: There and back again. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol. 4108, pp. 194–207. Springer, Heidelberg (2006)
Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: Tinycals: step by step tacticals. In: Proceedings of User Interface for Theorem Provers 2006. Electronic Notes in Theoretical Computer Science, vol. 174, pp. 125–142. Elsevier Science, Amsterdam (2006)
Sacerdoti Coen, C., Zacchiroli, S.: Spurious disambiguation errors and how to get rid of them. Journal of Mathematics in Computer Science, special issue on Management of Mathematical Knowledge 2, 355–378 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sacerdoti Coen, C., Tassi, E. (2009). Natural Deduction Environment for Matita. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds) Intelligent Computer Mathematics. CICM 2009. Lecture Notes in Computer Science(), vol 5625. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02614-0_40
Download citation
DOI: https://doi.org/10.1007/978-3-642-02614-0_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02613-3
Online ISBN: 978-3-642-02614-0
eBook Packages: Computer ScienceComputer Science (R0)