{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:22Z","timestamp":1774837822290,"version":"3.50.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2007,6,21]],"date-time":"2007-06-21T00:00:00Z","timestamp":1182384000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,8,20]]},"DOI":"10.1007\/s10817-007-9070-5","type":"journal-article","created":{"date-parts":[[2007,6,20]],"date-time":"2007-06-20T07:02:08Z","timestamp":1182322928000},"page":"109-139","source":"Crossref","is-referenced-by-count":44,"title":["User Interaction with the Matita Proof Assistant"],"prefix":"10.1007","volume":"39","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Zacchiroli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,6,21]]},"reference":[{"key":"9070_CR1","unstructured":"Aitken, S.: Problem solving in interactive proof: a knowledge-modelling approach. In: European Conference on Artificial Intelligence (ECAI), pp. 335\u2013339 (1996)"},{"issue":"2","key":"9070_CR2","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1006\/jsco.1997.0175","volume":"25","author":"S. Aitken","year":"1998","unstructured":"Aitken, S., Gray, P., Melham, T., Thomas, M.: Interactive theorem proving: an empirical study of user activity. J. Symb. Comput. 25(2), 263\u2013284 (1998)","journal-title":"J. Symb. Comput."},{"issue":"1\u20133","key":"9070_CR3","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1023\/A:1022907629104","volume":"38","author":"A. Asperti","year":"2003","unstructured":"Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical knowledge management in HELM. Ann. Math. Artif. Intell. 38(1\u20133), 27\u201346 (2003)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9070_CR4","doi-asserted-by":"crossref","unstructured":"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\u201332 (2004)","DOI":"10.1007\/11617990_2"},{"key":"9070_CR5","unstructured":"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"},{"key":"9070_CR6","unstructured":"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"},{"key":"9070_CR7","doi-asserted-by":"crossref","unstructured":"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\u201323 (2003)","DOI":"10.1007\/978-3-540-45155-6_2"},{"key":"9070_CR8","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/3-540-46419-0_3"},{"key":"9070_CR9","doi-asserted-by":"crossref","unstructured":"Bancerek, G.: On the structure of Mizar types. Electron. Notes Theor. Comput. Sci. 85(7), (2003)","DOI":"10.1016\/S1571-0661(04)80758-8"},{"key":"9070_CR10","doi-asserted-by":"crossref","unstructured":"Bancerek, G., Rudnicki, P.: Information retrieval in MML. In: Proceedings of the Mathematical Knowledge 2003. LNCS, vol. 2594 (2003)","DOI":"10.1007\/3-540-36469-2_10"},{"key":"9070_CR11","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/s001650050049","volume":"11","author":"Y. Bertot","year":"1999","unstructured":"Bertot, Y.: The CtCoq System: design and architecture. Form. Asp. Comput. 11, 225\u2013243 (1999)","journal-title":"Form. Asp. Comput."},{"key":"9070_CR12","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Kahn, G., Th\u00e9ry, L.: Proof by pointing. In: Symposium on Theoretical Aspects Computer Software (STACS). LNCS, vol. 789 (1994)","DOI":"10.1007\/3-540-57887-0_94"},{"issue":"4","key":"9070_CR13","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B. Buchberger","year":"2006","unstructured":"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\u2013504 (December 2006)","journal-title":"Journal of Applied Logic"},{"key":"9070_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0147-5","volume-title":"Automated Theory Formation in Pure Mathematics","author":"S. Colton","year":"2002","unstructured":"Colton, S.: Automated Theory Formation in Pure Mathematics. Springer, Berlin Heidelberg New York (2002)"},{"issue":"1-2","key":"9070_CR15","first-page":"113","volume":"65","author":"T. Coquand","year":"2005","unstructured":"Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. Fundam. Inform. 65(1-2), 113\u2013134 (2005)","journal-title":"Fundam. Inform."},{"key":"9070_CR16","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive coq repository at Nijmegen. In: MKM, pp. 88\u2013103 (2004)","DOI":"10.1007\/978-3-540-27818-4_7"},{"key":"9070_CR17","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: a mechanised logic of computation. In: LNCS, vol. 78 (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"9070_CR18","unstructured":"Hutter, D.: Towards a generic management of change. In: Workshop on Computer-supported Mathematical Theory Development, IJCAR (2004)"},{"issue":"3","key":"9070_CR19","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1023\/B:JLLI.0000028393.47593.b8","volume":"13","author":"F. Kamareddine","year":"2004","unstructured":"Kamareddine, F., Nederpelt, R.: A Refinement of de Bruijns formal language of mathematics. J. Logic, Lang. Inf. 13(3), 287\u2013340 (2004)","journal-title":"J. Logic, Lang. Inf."},{"issue":"1","key":"9070_CR20","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Luo, Z.: Coercive subtyping. J. Log. Comput. 9(1), 105\u2013130 (1999)","journal-title":"J. Log. Comput."},{"issue":"1","key":"9070_CR21","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/j.entcs.2005.11.021","volume":"151","author":"R.L. McCasland","year":"2006","unstructured":"McCasland, R.L., Bundy, A., Smith, P.F.: Ascertaining mathematical theorems. Electron. Notes Theor. Comput. Sci. 151(1), 21\u201338 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"9070_CR22","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"W. McCune","year":"1997","unstructured":"McCune, W., Wos, L.: Otter-The CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211\u2013220 (1997)","journal-title":"J. Autom. Reason."},{"key":"9070_CR23","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based Theorem Proving. vol. 1, pp. 371\u2013443. Elsevier and MIT Press. ISBN-0-262-18223-8 (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"9070_CR24","doi-asserted-by":"crossref","unstructured":"Obua, S.: Conservative overloading in higher-order logic. In: Rewriting Techniques and Applications. LNCS, vol. 4098, pp. 212\u2013226 (July 2006)","DOI":"10.1007\/11805618_16"},{"key":"9070_CR25","unstructured":"Padovani, L.: MathML formatting. PhD thesis, University of Bologna (2003)"},{"key":"9070_CR26","doi-asserted-by":"crossref","unstructured":"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\u2013207 (2006)","DOI":"10.1007\/11812289_16"},{"key":"9070_CR27","doi-asserted-by":"crossref","unstructured":"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\u201344 (2003)","DOI":"10.1007\/3-540-36469-2_3"},{"key":"9070_CR28","unstructured":"Sacerdoti Coen, C.: Mathematical knowledge management and interactive theorem proving. PhD thesis, University of Bologna (2004)"},{"key":"9070_CR29","doi-asserted-by":"crossref","unstructured":"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\u2013142 ISSN: 1571\u20130661 (May 2007)","DOI":"10.1016\/j.entcs.2006.09.026"},{"key":"9070_CR30","doi-asserted-by":"crossref","unstructured":"Sacerdoti Coen, C., Zacchiroli, S.: Efficient ambiguous parsing of mathematical formulae. In: Proceedings of Mathematical Knowledge Management 2004. LNCS, vol. 3119, pp. 347\u2013362 (2004)","DOI":"10.1007\/978-3-540-27818-4_25"},{"key":"9070_CR31","doi-asserted-by":"crossref","unstructured":"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\u201339 (1997)","DOI":"10.1145\/238218.238281"},{"issue":"2","key":"9070_CR32","first-page":"173","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: The CADE-20 automated theorem proving competition. AI Commun. 19(2), 173\u2013181 (2006)","journal-title":"AI Commun."},{"key":"9070_CR33","doi-asserted-by":"crossref","unstructured":"Syme, D.: A new interface for HOL \u2013 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\u2013339 (1995)","DOI":"10.1007\/3-540-60275-5_74"},{"issue":"3","key":"9070_CR34","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/s001650050054","volume":"11","author":"K. Takahashi","year":"1999","unstructured":"Takahashi, K., Hagiya, M.: Proving as editing HOL tactics. Form. Asp. Comput. 11(3), 343\u2013357 (1999)","journal-title":"Form. Asp. Comput."},{"key":"9070_CR35","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic.. In: TPHOLs, pp. 307\u2013322 (1997)","DOI":"10.1007\/BFb0028402"},{"key":"9070_CR36","unstructured":"Werner, B.: Une th\u00e9orie des constructions inductives. PhD thesis, Universit\u00e9 Paris VII (1994)"},{"key":"9070_CR37","unstructured":"Zacchiroli, S.: User interaction widgets for interactive theorem proving. PhD thesis, University of Bologna (2007)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9070-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-007-9070-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9070-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:47Z","timestamp":1559251307000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-007-9070-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6,21]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,8,20]]}},"alternative-id":["9070"],"URL":"https:\/\/doi.org\/10.1007\/s10817-007-9070-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6,21]]}}}