User Interaction with the Matita Proof Assistant

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. Keywords Proof assistant · Interactive theorem proving · Digital libraries · XML · Mathematical knowledge management · Authoring

• Type: Journal
• Year: 2007
• Where: JAR
• Authors: Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
• Keywords: Distinctive Features, JAR 2007, Mathematical Knowledge Management, Searchable Knowledge Base