Title
User Interaction with the Matita Proof Assistant
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.
Year
DOI
Venue
2007
10.1007/s10817-007-9070-5
J. Autom. Reasoning
Keywords
Field
DocType
Proof assistant,Interactive theorem proving,Digital libraries,XML,Mathematical knowledge management,Authoring
Programming language,XML,Computer science,Mathematical knowledge management,Knowledge base,Digital library,Rendering (computer graphics),Syntax,Semantics,Proof assistant
Journal
Volume
Issue
ISSN
39
2
0168-7433
Citations 
PageRank 
References 
48
2.79
26
Authors
4
Name
Order
Citations
PageRank
Andrea Asperti184975.19
Claudio Sacerdoti Coen238440.66
Enrico Tassi332721.79
Stefano Zacchiroli442637.60