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 Asperti | 1 | 849 | 75.19 |
Claudio Sacerdoti Coen | 2 | 384 | 40.66 |
Enrico Tassi | 3 | 327 | 21.79 |
Stefano Zacchiroli | 4 | 426 | 37.60 |