caa a22 4500 463182936 CHVBK 20180406164844.0 cr unu---uuuuu 170326e20070801xx s 000 0 eng 10.1007/s10817-007-9070-5 doi (NATIONALLICENCE)springer-10.1007/s10817-007-9070-5 User Interaction with the Matita Proof Assistant [Elektronische Daten] [Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli] 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. Springer Science+Business Media, Inc., 2007 Proof assistant nationallicence Interactive theorem proving nationallicence Digital libraries nationallicence XML nationallicence Mathematical knowledge management nationallicence Authoring nationallicence Asperti Andrea Department of Computer Science, University of Bologna, Mura Anteo Zamboni, 7-40127, Bologna, Italy aut Sacerdoti Coen Claudio Department of Computer Science, University of Bologna, Mura Anteo Zamboni, 7-40127, Bologna, Italy aut Tassi Enrico Department of Computer Science, University of Bologna, Mura Anteo Zamboni, 7-40127, Bologna, Italy aut Zacchiroli Stefano Department of Computer Science, University of Bologna, Mura Anteo Zamboni, 7-40127, Bologna, Italy aut Journal of Automated Reasoning Springer Netherlands 39/2(2007-08-01), 109-139 0168-7433 39:2<109 2007 39 10817 https://doi.org/10.1007/s10817-007-9070-5 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-007-9070-5 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Asperti Andrea Department of Computer Science, University of Bologna, Mura Anteo Zamboni, 7-40127, Bologna, Italy aut NATIONALLICENCE 700 1- Sacerdoti Coen Claudio Department of Computer Science, University of Bologna, Mura Anteo Zamboni, 7-40127, Bologna, Italy aut NATIONALLICENCE 700 1- Tassi Enrico Department of Computer Science, University of Bologna, Mura Anteo Zamboni, 7-40127, Bologna, Italy aut NATIONALLICENCE 700 1- Zacchiroli Stefano Department of Computer Science, University of Bologna, Mura Anteo Zamboni, 7-40127, Bologna, Italy aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Springer Netherlands 39/2(2007-08-01), 109-139 0168-7433 39:2<109 2007 39 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer