User interaction with the matita proof assistant

Andrea Asperti; Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli

doi:10.1007/s10817-007-9070-5

User interaction with the matita proof assistant

Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli

University of Bologna

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Pages (from-to)	109-139
Number of pages	31
Journal	Journal of Automated Reasoning
Volume	39
Issue number	2
DOIs	https://doi.org/10.1007/s10817-007-9070-5
Publication status	Published - 1 Aug 2007
Externally published	Yes

Keywords

Authoring
Digital libraries
Interactive theorem proving
Mathematical knowledge management
Proof assistant
XML

Access to Document

10.1007/s10817-007-9070-5

Cite this

@article{a39923c1e69643b9bef8f9dcb3943e19,

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.",

keywords = "Authoring, Digital libraries, Interactive theorem proving, Mathematical knowledge management, Proof assistant, XML",

author = "Andrea Asperti and \{Sacerdoti Coen\}, Claudio and Enrico Tassi and Stefano Zacchiroli",

year = "2007",

month = aug,

day = "1",

doi = "10.1007/s10817-007-9070-5",

language = "English",

volume = "39",

pages = "109--139",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

number = "2",

}

TY - JOUR

T1 - User interaction with the matita proof assistant

AU - Asperti, Andrea

AU - Sacerdoti Coen, Claudio

AU - Tassi, Enrico

AU - Zacchiroli, Stefano

PY - 2007/8/1

Y1 - 2007/8/1

N2 - 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.

AB - 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.

KW - Authoring

KW - Digital libraries

KW - Interactive theorem proving

KW - Mathematical knowledge management

KW - Proof assistant

KW - XML

U2 - 10.1007/s10817-007-9070-5

DO - 10.1007/s10817-007-9070-5

M3 - Article

AN - SCOPUS:34548285418

SN - 0168-7433

VL - 39

SP - 109

EP - 139

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 2

ER -

User interaction with the matita proof assistant

Abstract

Keywords

Access to Document

Fingerprint

Cite this