{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:59:28Z","timestamp":1773097168245,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642224379","type":"print"},{"value":"9783642224386","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_7","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T22:21:44Z","timestamp":1311027704000},"page":"64-69","source":"Crossref","is-referenced-by-count":36,"title":["The Matita Interactive Theorem Prover"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[]},{"given":"Wilmer","family":"Ricciotti","sequence":"additional","affiliation":[]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","first-page":"1","volume":"1","author":"A. Asperti","year":"2008","unstructured":"Asperti, A., Armentano, C.: A page in number theory. Journal of Formalized Reasoning\u00a01, 1\u201323 (2008)","journal-title":"Journal of Formalized Reasoning"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11617990_2","volume-title":"Types for Proofs and Programs","author":"A. Asperti","year":"2006","unstructured":"Asperti, A., Guidi, F., Coen, C.S., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: Whelp. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 17\u201332. Springer, Heidelberg (2006)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-02444-3_2","volume-title":"Types for Proofs and Programs","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W.: About the formalization of some results by chebyshev in number theory. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 19\u201331. Springer, Heidelberg (2009)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-03359-9_8","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 84\u201398. Springer, Heidelberg (2009)"},{"issue":"2","key":"7_CR5","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A. Asperti","year":"2007","unstructured":"Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. J. Autom. Reasoning\u00a039(2), 109\u2013139 (2007)","journal-title":"J. Autom. Reasoning"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Asperti, A., Tassi, E.: An interactive driver for goal directed proof strategies. In: Proc. of UITP 2008. ENTCS, vol.\u00a0226, pp. 89\u2013105 (2009)","DOI":"10.1016\/j.entcs.2008.12.099"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-14128-7_23","volume-title":"Intelligent Computer Mathematics","author":"A. Asperti","year":"2010","unstructured":"Asperti, A., Tassi, E.: Smart matching. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 263\u2013277. Springer, Heidelberg (2010)"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Asperti, A., Tassi, E.: Superposition as a logical glue. In: Proc. of TYPES 2009, EPTCS (2010) (to appear)","DOI":"10.4204\/EPTCS.53.1"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof general: A generic tool for proof development. In: Graf, S. (ed.) TACAS 2000. LNCS, vol.\u00a01785, p. 38. Springer, Heidelberg (2000)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"B.E. Aydemir","year":"2005","unstructured":"Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Babu, C. S., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s001650050049","volume":"11","author":"Y. Bertot","year":"1999","unstructured":"Bertot, Y.: The CtCoq system: Design and architecture. Formal Aspects of Computing\u00a011, 225\u2013243 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"7_CR12","unstructured":"The CerCo website, http:\/\/cerco.cs.unibo.it"},{"issue":"1-2","key":"7_CR13","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10817-009-9136-7","volume":"44","author":"C.S. Coen","year":"2010","unstructured":"Coen, C.S.: Declarative representation of proof terms. J. Autom. Reasoning\u00a044(1-2), 25\u201352 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"7_CR14","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. Technical Report NASA\/CP-2003-212448, Nasa technical reports (2003)"},{"key":"7_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"issue":"1","key":"7_CR16","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Luo, Z.: Coercive subtyping. J. Logic and Computation\u00a09(1), 105\u2013130 (1999)","journal-title":"J. Logic and Computation"},{"issue":"2","key":"7_CR17","doi-asserted-by":"publisher","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. of Autom. Reasoning\u00a018(2), 211\u2013220 (1997)","journal-title":"J. of Autom. Reasoning"},{"issue":"10","key":"7_CR18","doi-asserted-by":"publisher","first-page":"1575","DOI":"10.1016\/j.ic.2005.05.010","volume":"204","author":"J. Meng","year":"2006","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Inf. Comput.\u00a0204(10), 1575\u20131596 (2006)","journal-title":"Inf. Comput."},{"key":"7_CR19","unstructured":"The Mizar proof-assistant, http:\/\/mizar.uwb.edu.pl\/"},{"key":"7_CR20","first-page":"51","volume":"1","author":"C.S. Coen","year":"2008","unstructured":"Coen, C.S., Tassi, E.: A constructive and formal proof of Lebesgue\u2019s dominated convergence theorem in the interactive theorem prover Matita. Journal of Formalized Reasoning\u00a01, 51\u201389 (2008)","journal-title":"Journal of Formalized Reasoning"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-68103-8_11","volume-title":"Types for Proofs and Programs","author":"C. Sacerdoti Coen","year":"2008","unstructured":"Sacerdoti Coen, C., Tassi, E.: Working with mathematical structures in type theory. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 157\u2013172. Springer, Heidelberg (2008)"},{"key":"7_CR22","first-page":"125","volume-title":"Proc. of UITP 2006. ENTCS","author":"C.S. Coen","year":"2006","unstructured":"Coen, C.S., Tassi, E., Zacchiroli, S.: Tinycals: step by step tacticals. In: Proc. of UITP 2006. ENTCS, vol.\u00a0174, pp. 125\u2013142. Elsevier Science, Amsterdam (2006)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-27818-4_25","volume-title":"Mathematical Knowledge Management","author":"C.S. Coen","year":"2004","unstructured":"Coen, C.S., Zacchiroli, S.: Efficient ambiguous parsing of mathematical formulae. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 347\u2013362. Springer, Heidelberg (2004)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-74464-1_16","volume-title":"Types for Proofs and Programs","author":"M. Sozeau","year":"2007","unstructured":"Sozeau, M.: Subset coercions in coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"key":"7_CR26","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/AIC-2010-0469","volume":"23","author":"G. Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The CADE-22 automated theorem proving system competition - CASC-22. AI Commun.\u00a023, 47\u201359 (2010)","journal-title":"AI Commun."},{"key":"7_CR27","unstructured":"The Coq Development Team. The Coq proof assistant reference manual, http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 307\u2013322. Springer, Heidelberg (1997)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M.T. Wenzel","year":"1999","unstructured":"Wenzel, M.T.: Isar - A generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013184. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,21]],"date-time":"2020-06-21T11:44:56Z","timestamp":1592739896000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}