Matita is an experimental

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof edi ...

under development at the

Computer Science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...

Department of the

University of Bologna The University of Bologna (, abbreviated Unibo) is a Public university, public research university in Bologna, Italy. Teaching began around 1088, with the university becoming organised as guilds of students () by the late 12th century. It is the ...

. It is a tool aiding the development of

formal proof In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (known as well-formed formulas when relating to formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the s ...

s by man–machine collaboration, providing a programming environment where

formal specification In computer science, formal specifications are mathematically based techniques whose purpose is to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verify ...

s, executable algorithms and automatically verifiable correctness certificates naturally coexist. Matita is based on a

dependent type In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers lik ...

system known as the calculus of (co)inductive constructions (a derivative of the

calculus of constructions In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reaso ...

), and is compatible, to some extent, with

Coq Coenzyme Q10 (CoQ10 ), also known as ubiquinone, is a naturally occurring biochemical cofactor (coenzyme) and an antioxidant produced by the human body. It can also be obtained from dietary sources, such as meat, fish, seed oils, vegetables, ...

. The word "matita" means "pencil" in Italian (a simple and widespread editing tool). It is a reasonably small and simple application, whose architectural and software complexity is meant to be mastered by students, providing a tool particularly suited for testing innovative ideas and solutions. Matita adopts a

tactic Tactic(s) or Tactical may refer to: * Tactic (method), a conceptual action implemented as one or more specific tasks ** Military tactics, the disposition and maneuver of units on a particular sea or battlefield ** Chess tactics ** Political tacti ...

-based editing mode; (

XML Extensible Markup Language (XML) is a markup language and file format for storing, transmitting, and reconstructing data. It defines a set of rules for encoding electronic document, documents in a format that is both human-readable and Machine-r ...

-encoded) proof objects are produced for storage and exchange.

Main features

Existential variables are native in Matita, allowing a simpler management of dependent goals. Matita implements a bidirectional

type inference Type inference, sometimes called type reconstruction, refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some bran ...

algorithm exploiting both inferred and expected types. The power of the type inference system (refiner) is further augmented by a mechanism of hints that helps in synthesizing unifiers in particular situations specified by the user. Matita supports a sophisticated disambiguation strategy based on a dialog between the

parser Parsing, syntax analysis, or syntactic analysis is a process of analyzing a string of symbols, either in natural language, computer languages or data structures, conforming to the rules of a formal grammar by breaking it into parts. The term '' ...

and the typechecker. At the interactive level, the system implements a small step execution of structured tactics allowing a much better management of the proof development, and naturally leading to more structured and readable scripts.

Applications

Matita has been employed i
CerCo
(Certified Complexity): a

European Project focused on the development of a formally verified, complexity preserving

compiler In computing, a compiler is a computer program that Translator (computing), translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primaril ...

from a large subset of C to the

assembly language In computing, assembly language (alternatively assembler language or symbolic machine code), often referred to simply as assembly and commonly abbreviated as ASM or asm, is any low-level programming language with a very strong correspondence bet ...

of a

MCS-51 The Intel MCS-51 (commonly termed 8051) is a single-chip microcontroller (MCU) series developed by Intel in 1980 for use in embedded systems. The architect of the Intel MCS-51 instruction set was John H. Wharton.. Intel's original versions w ...

microprocessor.

Documentation

The Matita tutorial Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen "Matita Tutorial
Journal of Formalized Reasoning, V.7, n. 2, 2014, Pages 91-199
provides a pragmatic introduction to the main functionalities of the Matita interactive theorem prover, offering a guided tour through a set of non-trivial examples in the field of

software specification In computer science, formal specifications are mathematically based techniques whose purpose is to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verify ...

and verification.

References

External links

* * {{ML programming Proof assistants Free theorem provers Dependently typed languages Educational math software OCaml software Free software programmed in OCaml Functional languages

Main features

Applications

Documentation

See also

References

External links