Matita (means pencil in italian) is an experimental, interactive theorem prover.
An interactive prover is a software tool aiding the development of formal proofs by man-machine collaboration. It provides a formal language where mathematical definitions, executable algorithms and theorems cohexist, and an interactive environment keeping the current status of the proof, and updating it according to commands (usually called tactics) issued by the user.
Matita is based on a Dependent Type System known as the Calculus of Inductive Constructions.
It embeds key computational constructs of functional programming languages: functions can be defined by (well-founded) recursion, and are live entities that can be tested and executed.
At the same time, proofs are an integrated part of the formalism, allowing, via the Curry Howard isomorphism, a smooth interplay between specification, implementation and verification: proofs are objects of the language, and can be treated as normal data, naturally leading to a programming style akin to proof-carrying-code, where chunks of software come equipped with proofs of (some of) their properties.
Matita is part of HELM, an Hypertextual, Electronic Library of Mathematics, developed at the Computer Science Department, University of Bologna, Italy.
Website: github.com/LPCIC/matita
Support:
Developer: Andrea Asperti, Ferruccio Guidi, Luca Padovani, Enrico Tassi, Claudio Sacerdoti Coen, and Stefano Zacchiroli
License: GNU General Public License v2.0
Related Software
| Proof Assistants | |
|---|---|
| Rocq Prover | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Lean | Programming language and theorem prover |
| Agda | Interactive system for writing and checking proofs |
| F* | Functional language for verified programs with dependent refinement types |
| HOL4 | Interactive higher-order logic environment for rigorous theorem development |
| Aya | Dependently typed language for formalisation and certified programming |
| Lambdapi | Logical framework for defining and checking expressive type systems |
| HOL Light | Lightweight higher-order logic system with a small trusted kernel |
| PVS | Specification and verification suite for analysing complex systems |
| LISA | Scala-based platform for formal mathematics and automated reasoning |
Read our verdict in the software roundup.
 Explore our comprehensive directory of recommended free and open source software. Our carefully curated collection spans every major software category.This directory is part of our ongoing series of informative articles for Linux enthusiasts. It features hundreds of detailed reviews, along with open source alternatives to proprietary solutions from major corporations such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. You’ll also find interesting projects to try, hardware coverage, free programming books and tutorials, and much more. Discovered a useful open source Linux program that we haven’t covered yet? Let us know by completing this form. |
Please read our Comment Policy before commenting.