User interaction with the Matita proof assistant
A Asperti, C Sacerdoti Coen, E Tassi… - Journal of Automated …, 2007 - Springer
Journal of Automated Reasoning, 2007•Springer
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.
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.
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.
Springer
