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, characterized mostly by the organization of the library as a searchable knowledge base, the emphasis on a high-quality notational rendering, and the complex interplay between syntax, presentation, and semantics.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Aitken, S.: Problem solving in interactive proof: a knowledge-modelling approach. In: European Conference on Artificial Intelligence (ECAI), pp. 335–339 (1996)
Aitken, S., Gray, P., Melham, T., Thomas, M.: Interactive theorem proving: an empirical study of user activity. J. Symb. Comput. 25(2), 263–284 (1998)
Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical knowledge management in HELM. Ann. Math. Artif. Intell. 38(1–3), 27–46 (2003)
Asperti, A., Guidi, F., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: Whelp. In: Post-proceedings of the Types 2004 International Conference. LNCS, vol. 3839, pp. 17–32 (2004)
Asperti, A., Padovani, L., Sacerdoti Coen, C., Schena, I.: Content-centric logical environments. Short presentation at the Fifteenth IEEE Symposium on Logic in Computer Science, 2000
Asperti, A., Padovani, L., Sacerdoti Coen, C., Schena, I.: XML, stylesheets and the re-mathematization of formal content. In: Proceedings of EXTREME Markup Languages, 2001
Asperti, A., Wegner, B.: An approach to machine-understandable representation of the mathematical information in digital documents. In: Electronic Information and Communication in Mathematics. LNCS, vol. 2730, pp. 14–23 (2003)
Aspinall, D.: Proof general: A generic tool for proof development. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000. LNCS, vol. 1785 (2000)
Bancerek, G.: On the structure of Mizar types. Electron. Notes Theor. Comput. Sci. 85(7), (2003)
Bancerek, G., Rudnicki, P.: Information retrieval in MML. In: Proceedings of the Mathematical Knowledge 2003. LNCS, vol. 2594 (2003)
Bertot, Y.: The CtCoq System: design and architecture. Form. Asp. Comput. 11, 225–243 (1999)
Bertot, Y., Kahn, G., Théry, L.: Proof by pointing. In: Symposium on Theoretical Aspects Computer Software (STACS). LNCS, vol. 789 (1994)
Buchberger, B., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: towards computer-aided mathematical theory exploration. Journal of Applied Logic. 4(4), 470–504 (December 2006)
Colton, S.: Automated Theory Formation in Pure Mathematics. Springer, Berlin Heidelberg New York (2002)
Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. Fundam. Inform. 65(1-2), 113–134 (2005)
Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive coq repository at Nijmegen. In: MKM, pp. 88–103 (2004)
Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: a mechanised logic of computation. In: LNCS, vol. 78 (1979)
Hutter, D.: Towards a generic management of change. In: Workshop on Computer-supported Mathematical Theory Development, IJCAR (2004)
Kamareddine, F., Nederpelt, R.: A Refinement of de Bruijns formal language of mathematics. J. Logic, Lang. Inf. 13(3), 287–340 (2004)
Luo, Z.: Coercive subtyping. J. Log. Comput. 9(1), 105–130 (1999)
McCasland, R.L., Bundy, A., Smith, P.F.: Ascertaining mathematical theorems. Electron. Notes Theor. Comput. Sci. 151(1), 21–38 (2006)
McCune, W., Wos, L.: Otter-The CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211–220 (1997)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based Theorem Proving. vol. 1, pp. 371–443. Elsevier and MIT Press. ISBN-0-262-18223-8 (2001)
Obua, S.: Conservative overloading in higher-order logic. In: Rewriting Techniques and Applications. LNCS, vol. 4098, pp. 212–226 (July 2006)
Padovani, L.: MathML formatting. PhD thesis, University of Bologna (2003)
Padovani, L., Zacchiroli, S.: From notation to semantics: there and back again. In: Proceedings of Mathematical Knowledge Management 2006. Lectures Notes in Artificial Intelligence, vol. 3119, pp. 194–207 (2006)
Sacerdoti Coen, C.: From proof-assistans to distributed libraries of mathematics: tips and pitfalls. In: Proceedings of the Mathematical Knowledge Management 2003. LNCS, vol. 2594, pp. 30–44 (2003)
Sacerdoti Coen, C.: Mathematical knowledge management and interactive theorem proving. PhD thesis, University of Bologna (2004)
Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: Tinycals: step by step tacticals. In: Proceedings of User Interface for Theorem Provers. ENTCS 174(2), pp. 125–142 ISSN: 1571–0661 (May 2007)
Sacerdoti Coen, C., Zacchiroli, S.: Efficient ambiguous parsing of mathematical formulae. In: Proceedings of Mathematical Knowledge Management 2004. LNCS, vol. 3119, pp. 347–362 (2004)
Shneiderman, B.: Direct manipulation for comprehensible, predictable and controllable user interfaces. In: Proceedings of the 2nd International Conference on Intelligent User Interfaces. New York, NY, pp. 33–39 (1997)
Sutcliffe, G.: The CADE-20 automated theorem proving competition. AI Commun. 19(2), 173–181 (2006)
Syme, D.: A new interface for HOL – ideas, issues and implementation. In: Proceedings of Higher-order Logic Theorem Proving and its Applications. 8th International Workshop, TPHOLs 1995. LNCS, vol. 971, pp. 324–339 (1995)
Takahashi, K., Hagiya, M.: Proving as editing HOL tactics. Form. Asp. Comput. 11(3), 343–357 (1999)
Wenzel, M.: Type classes and overloading in higher-order logic.. In: TPHOLs, pp. 307–322 (1997)
Werner, B.: Une théorie des constructions inductives. PhD thesis, Université Paris VII (1994)
Zacchiroli, S.: User interaction widgets for interactive theorem proving. PhD thesis, University of Bologna (2007)
Author information
Authors and Affiliations
Corresponding author
Additional information
“We are nearly bug-free” – CSC, Oct. 2005.
Rights and permissions
About this article
Cite this article
Asperti, A., Sacerdoti Coen, C., Tassi, E. et al. User Interaction with the Matita Proof Assistant. J Autom Reasoning 39, 109–139 (2007). https://doi.org/10.1007/s10817-007-9070-5
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-007-9070-5