Abstract
This article describes a prototype implementation of a web interface for the Matita proof assistant [2]. The motivations behind our work are similar to those of several recent, related efforts [7,9,1,8] (see also [6]).
The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alama, J., Brink, K., Mamane, L., Urban, J.: Large Formal Wikis: Issues and Solutions. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 133–148. Springer, Heidelberg (2011)
Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita Interactive Theorem Prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64–69. Springer, Heidelberg (2011)
Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Journal of Automated Reasoning 39(2), 109–139 (2007)
Aspinall, D.: Proof General: A Generic Tool for Proof Development. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 38–43. Springer, Heidelberg (2000)
Bertot, Y., Théry, L.: A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation 25, 161–194 (1998)
Geuvers, H.: Proof Assistants: history, ideas and future. Sadhana 34(1), 3–25 (2009)
Kaliszyk, C.: Web interfaces for proof assistants. Electr. Notes Theor. Comput. Sci. 174(2), 49–61 (2007)
Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: A Tool for Proof Re-animation. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol. 6167, pp. 440–454. Springer, Heidelberg (2010)
Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A wiki for mizar: Motivation, considerations, and initial prototype. CoRR, abs/1005.4552 (2010)
Wenzel, M.: Isabelle as Document-Oriented Proof Assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 244–259. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asperti, A., Ricciotti, W. (2012). A Web Interface for Matita. In: Jeuring, J., et al. Intelligent Computer Mathematics. CICM 2012. Lecture Notes in Computer Science(), vol 7362. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31374-5_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-31374-5_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31373-8
Online ISBN: 978-3-642-31374-5
eBook Packages: Computer ScienceComputer Science (R0)