The Matita Interactive Theorem Prover

Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen; Enrico Tassi

doi:10.1007/978-3-642-22438-6_7

The Matita Interactive Theorem Prover

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Matita is an interactive theorem prover being developed by the Helm team at the University of Bologna. Its stable version 0.5.x may be downloaded at http://matita.cs.unibo.it . The tool originated in the European project MoWGLI as a set of XML-based tools aimed to provide a mathematician-friendly web-interface to repositories of formal mathematical knoweldge, supporting advanced content-based functionalities for querying, searching and browsing the library. It has since then evolved into a fully fledged ITP, specifically designed as a light-weight, but competitive system, particularly suited for the assessment of innovative ideas, both at foundational and logical level. In this paper, we give an account of the whole system, its peculiarities and its main applications.

Original language	English
Title of host publication	Automated Deduction - CADE-23
Subtitle of host publication	23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings
Publisher	Springer Berlin Heidelberg
Pages	64-69
Number of pages	6
ISBN (Electronic)	978-3-642-22438-6
ISBN (Print)	978-3-642-22437-9
DOIs	https://doi.org/10.1007/978-3-642-22438-6_7
Publication status	Published - 2011

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	6803
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-642-22438-6_7

http://link.springer.com/chapter/10.1007%2F978-3-642-22438-6_7

Cite this

Asperti, A., Ricciotti, W., Coen, C. S., & Tassi, E. (2011). The Matita Interactive Theorem Prover. In Automated Deduction - CADE-23: 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings (pp. 64-69). (Lecture Notes in Computer Science; Vol. 6803). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_7

@inproceedings{75cf5d7ae4fa44f8ae3c56398419384e,

title = "The Matita Interactive Theorem Prover",

abstract = "Matita is an interactive theorem prover being developed by the Helm team at the University of Bologna. Its stable version 0.5.x may be downloaded at http://matita.cs.unibo.it . The tool originated in the European project MoWGLI as a set of XML-based tools aimed to provide a mathematician-friendly web-interface to repositories of formal mathematical knoweldge, supporting advanced content-based functionalities for querying, searching and browsing the library. It has since then evolved into a fully fledged ITP, specifically designed as a light-weight, but competitive system, particularly suited for the assessment of innovative ideas, both at foundational and logical level. In this paper, we give an account of the whole system, its peculiarities and its main applications.",

author = "Andrea Asperti and Wilmer Ricciotti and Coen, {Claudio Sacerdoti} and Enrico Tassi",

year = "2011",

doi = "10.1007/978-3-642-22438-6_7",

language = "English",

isbn = "978-3-642-22437-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "64--69",

booktitle = "Automated Deduction - CADE-23",

}

The Matita Interactive Theorem Prover. / Asperti, Andrea; Ricciotti, Wilmer; Coen, Claudio Sacerdoti et al.

Automated Deduction - CADE-23: 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings. Springer Berlin Heidelberg, 2011. p. 64-69 (Lecture Notes in Computer Science; Vol. 6803).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - The Matita Interactive Theorem Prover

AU - Asperti, Andrea

AU - Ricciotti, Wilmer

AU - Coen, Claudio Sacerdoti

AU - Tassi, Enrico

PY - 2011

Y1 - 2011

N2 - Matita is an interactive theorem prover being developed by the Helm team at the University of Bologna. Its stable version 0.5.x may be downloaded at http://matita.cs.unibo.it . The tool originated in the European project MoWGLI as a set of XML-based tools aimed to provide a mathematician-friendly web-interface to repositories of formal mathematical knoweldge, supporting advanced content-based functionalities for querying, searching and browsing the library. It has since then evolved into a fully fledged ITP, specifically designed as a light-weight, but competitive system, particularly suited for the assessment of innovative ideas, both at foundational and logical level. In this paper, we give an account of the whole system, its peculiarities and its main applications.

AB - Matita is an interactive theorem prover being developed by the Helm team at the University of Bologna. Its stable version 0.5.x may be downloaded at http://matita.cs.unibo.it . The tool originated in the European project MoWGLI as a set of XML-based tools aimed to provide a mathematician-friendly web-interface to repositories of formal mathematical knoweldge, supporting advanced content-based functionalities for querying, searching and browsing the library. It has since then evolved into a fully fledged ITP, specifically designed as a light-weight, but competitive system, particularly suited for the assessment of innovative ideas, both at foundational and logical level. In this paper, we give an account of the whole system, its peculiarities and its main applications.

U2 - 10.1007/978-3-642-22438-6_7

DO - 10.1007/978-3-642-22438-6_7

M3 - Conference contribution

SN - 978-3-642-22437-9

T3 - Lecture Notes in Computer Science

SP - 64

EP - 69

BT - Automated Deduction - CADE-23

PB - Springer Berlin Heidelberg

ER -

The Matita Interactive Theorem Prover

Abstract

Publication series

Access to Document

Fingerprint

Cite this