Matita swMATH ID: 6140 Software Authors: Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico Description: Matita (that means pencil in italian) is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna. An interactive prover is a software tool aiding the development of formal proofs by man-machine collaboration. It provides a formal language where mathematical definitions, executable algorithms and theorems cohexist, and an interactive environment keeping the current status of the proof, and updating it according to commands (usually called tactics) issued by the user. Homepage: http://matita.cs.unibo.it/ Keywords: refiner; type inference; interactive theorem prover; calculus of inductive constructions; {\tt Matita} Related Software: Coq; Mizar; Isabelle/HOL; Isabelle; Agda; Proof General; HOL Light; HOL; Isar; Lean; Whelp; Automath; Coq/SSReflect; CtCoq; ML; PVS; TPTP; LCF; Nuprl; C-CoRN Cited in: 74 Publications Standard Articles 3 Publications describing the Software, including 3 Publications in zbMATH Year Matita tutorial. Zbl 1451.68314Asperti, Andrea; Ricciotti, Wilmer; Coen, Claudio Sacerdoti 2014 The Matita interactive theorem prover. Zbl 1341.68179Asperti, Andrea; Ricciotti, Wilmer; Sacerdoti Coen, Claudio; Tassi, Enrico 2011 User interaction with the Matita proof assistant. Zbl 1132.68673Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano 2007 all top 5 Cited by 87 Authors 21 Asperti, Andrea 18 Sacerdoti Coen, Claudio 15 Tassi, Enrico 11 Ricciotti, Wilmer 4 Popescu, Andrei 4 Zacchiroli, Stefano 3 de Moura, Leonardo 3 Guidi, Ferruccio 3 Wenzel, Makarius 2 Blanchette, Jasmin Christian 2 Gonthier, Georges 2 Kunčar, Ondřej 2 Maietti, Maria Emilia 2 Roversi, Luca 2 Spitters, Bas 2 Sutcliffe, Geoff 2 Traytel, Dmitry 1 Armentano, Cristian 1 Aspinall, David 1 Autexier, Serge 1 Avigad, Jeremy 1 Benzmüller, Christoph Ewald 1 Blanqui, Frédéric 1 Bonichon, Richard 1 Bouzy, Aymeric 1 Calude, Cristian S. 1 Delahaye, David 1 Denney, Ewen 1 Dietrich, Dominik 1 Doligez, Damien 1 Dowek, Gilles 1 Fiedler, Armin 1 Fridlender, Daniel 1 Ganesh, Anumanthappa 1 Garillot, François 1 Gauthier, Thibault 1 Geuvers, Jan Herman 1 Govindan, Vediyappan 1 Gunasekaran, Nallappan 1 Hammachukiattikul, Porpattama 1 Heras, Jónathan 1 Huet, Gerard P. 1 Kahl, Wolfram 1 Kaliszyk, Cezary 1 Kfoury, Assaf J. 1 Komendantskaya, Ekaterina 1 Kong, Soonho 1 Krebbers, Robbert 1 Lange, Christoph 1 Lapets, Andrei 1 Lim, Chee Peng 1 Lochbihler, Andreas 1 Luo, Zhaohui 1 Lüth, Christoph 1 Mahboubi, Assia 1 Maletto, Giacomo 1 McKinna, James 1 Melo de Sousa, Simão 1 Mohanapriya, Arusamy 1 Moreira, Nelma 1 Müller, Dennis 1 Neumann, Thomas 1 Pagano, Miguel 1 Paolini, Luca 1 Passmore, Grant Olney 1 Pereira, David P. 1 Piccolo, Mauro 1 Pollack, Randy 1 Rabe, Florian 1 Rajchakit, Grienggrai 1 Rideau, Laurence 1 Sakaguchi, Kazuhiko 1 Sambin, Giovanni 1 Sato, Masahiko 1 Schulz, Ewaryst 1 Selsam, Daniel 1 Tankink, Carst 1 Taschner, Rudolf J. 1 Thompson, Declan 1 Valentini, Silvio 1 van der Hoeven, Joris 1 van der Weegen, Eelis 1 van Doorn, Floris 1 von Raumer, Jakob 1 Wagner, Marc Oliver 1 Wiedijk, Freek 1 Xue, Tao all top 5 Cited in 14 Serials 8 Journal of Automated Reasoning 6 Journal of Formalized Reasoning 4 MSCS. Mathematical Structures in Computer Science 3 Mathematics in Computer Science 2 Theoretical Computer Science 2 Journal of Symbolic Computation 2 Logical Methods in Computer Science 2 Journal of Logical and Algebraic Methods in Programming 1 AI Communications 1 Mathematical Logic Quarterly (MLQ) 1 Journal of Functional Programming 1 ACM Transactions on Computational Logic 1 Advances in Difference Equations 1 Studies on the Semantic Web all top 5 Cited in 11 Fields 71 Computer science (68-XX) 19 Mathematical logic and foundations (03-XX) 2 Number theory (11-XX) 1 Category theory; homological algebra (18-XX) 1 Real functions (26-XX) 1 Measure and integration (28-XX) 1 Special functions (33-XX) 1 Partial differential equations (35-XX) 1 Integral transforms, operational calculus (44-XX) 1 Numerical analysis (65-XX) 1 Quantum theory (81-XX) Citations by Year