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.
A.Asperti, C.Sacerdoti Coen, E. Tassi, S.Zacchiroli (2007). User Interaction with the Matita Proof Assistant. JOURNAL OF AUTOMATED REASONING, 39, Number 2, 109-139 [10.1007/s10817-007-9070-5].
User Interaction with the Matita Proof Assistant
ASPERTI, ANDREA;SACERDOTI COEN, CLAUDIO;TASSI, ENRICO;
2007
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.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
