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

under development at the

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

Department of the

University of Bologna The University of Bologna ( it, Alma Mater Studiorum – Università di Bologna, UNIBO) is a public research university in Bologna, Italy. Founded in 1088 by an organised guild of students (''studiorum''), it is the oldest university in continuo ...

. 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 (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the seque ...

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

formal specification In computer science, formal specifications are mathematically based techniques whose purpose are 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 verif ...

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

), and is compatible, to some extent, with

Coq Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...

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

-based editing mode; (

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

-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 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 branches of computer science and linguistics ...

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 the process of analyzing a string of symbols, either in natural language, computer languages or data structures, conforming to the rules of a formal grammar. The term ''parsing'' comes from Lati ...

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 translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs that ...

from a large subset of C to the

assembly language In computer programming, assembly language (or 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 be ...

of a MCS-51 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 are 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 verif ...

and

verification Verify or verification may refer to: General * Verification and validation, in engineering or quality management systems, is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets ...

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