Matita

From Wikipedia, the free encyclopedia

Matita
The Matita proof authoring interface.
Developed by	Matita team
Initial release	?
Written in	?
OS	GNU/Linux
Available in	English
Genre	Theorem proving
License	GPL
Website	http://matita.cs.unibo.it

Matita is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna.

Matita is based on the Calculus of (Co)Inductive Constructions (a derivative of Calculus of Constructions), and is compatible, at some extent, with Coq. 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 based editing mode; (XML-encoded) proof objects are produced for storage and exchange.

[edit] See also

• Curry-Howard
• Intuitionistic Type Theory

[edit] External links

• The Matita Proof Assistant