Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Matita
open-in-new
<h2 id="main-features">Main features</h2> <p>Existential variables are native in Matita, allowing a simpler management of dependent goals.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a> </p><p>Matita implements a bidirectional <a href="/facts/Type_inference/vX9K8Qhf">type inference</a> algorithm<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a> exploiting both inferred and expected types. </p><p>The power of the type inference system (refiner) is further augmented by a mechanism of hints<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a> that helps in synthesizing <a href="/facts/Unification_(computer_science)/4EPHSB1T">unifiers</a> in particular situations specified by the user. </p><p>Matita supports a sophisticated disambiguation strategy<a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a> based on a dialog between the <a href="/facts/Parsing/nRKB01S3">parser</a> and the <a href="/facts/Type_system/Tz0bAMS9">typechecker</a>. </p><p>At the interactive level, the system implements a small step execution of structured tactics<a class="footnote-ref" id="fnref:7" href="#fn:7"><sup>7</sup></a> allowing a much better management of the proof development, and naturally leading to more structured and readable scripts. </p> <h2 id="applications">Applications</h2> <p>Matita has been employed in <a href="http://cerco.cs.unibo.it/">CerCo</a> (Certified Complexity): a <a href="http://cordis.europa.eu/fp7/home_en.html">FP7</a> European Project focused on the development of a <a href="/facts/Formal_verification/BYD4GnJR">formally verified</a>, complexity preserving <a href="/facts/Compiler/WNfCDFJe">compiler</a> from a large subset of <a href="/facts/C_(programming_language)/Ky2No763">C</a> to the <a href="/facts/Assembly_language/7XuV0cla">assembly language</a> of a <a href="/facts/MCS-51/2bqJXGlv">MCS-51</a> microprocessor. </p> <h2 id="documentation">Documentation</h2> <p>The Matita tutorial<a class="footnote-ref" id="fnref:8" href="#fn:8"><sup>8</sup></a> 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 <a href="/facts/Software_specification/4q2oDkvS">software specification</a> and <a href="/facts/Software_verification/PczD7lsh">verification</a>. </p> <h2 id="see-also">See also</h2> <ul><li><a href="/facts/Curry%25E2%2580%2593Howard_correspondence/Q3eVu60u">Curry–Howard correspondence</a></li> <li><a href="/facts/Interactive_theorem_proving/hjFGxLPn">Interactive theorem proving</a></li> <li><a href="/facts/Intuitionistic_type_theory/qwkrpKlP">Intuitionistic type theory</a></li> <li><a href="/facts/List_of_proof_assistants/hjFGxLPn">List of proof assistants</a></li></ul> <h2 id="external-links">External links</h2> <ul><li><a href="https://web.archive.org/web/20230204212750/http://matita.cs.unibo.it/">The Matita Proof Assistant</a> at the <a href="/facts/Wayback_Machine/nmQ3a6JC">Wayback Machine</a> (archived 2023-02-04)</li> <li><a href="https://web.archive.org/web/20220521000852/http://cerco.cs.unibo.it/">CerCo Project</a> at the <a href="/facts/Wayback_Machine/nmQ3a6JC">Wayback Machine</a> (archived 2022-05-21)</li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi. "The Matita Interactive Theorem Prover": CADE-23, LNCS 6803, 2011, pp. 64-69. <a href="https://link.springer.com/chapter/10.1007%2F978-3-642-22438-6_7" target="_blank">https://link.springer.com/chapter/10.1007%2F978-3-642-22438-6_7</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>Asperti, A.; Ricciotti, W.; Sacerdoti Coen, C.; Tassi, E. (2009). "A compact kernel for the calculus of inductive constructions". Sādhanā. 34: 71–144. doi:10.1007/s12046-009-0003-3. <a href="https://doi.org/10.1007%2Fs12046-009-0003-3" target="_blank">https://doi.org/10.1007%2Fs12046-009-0003-3</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. "A new type for tactics": Technical Report UBLCS-2009-14. June 2009. <a href="http://matita.cs.unibo.it/PAPERS/plmms09.pdf" target="_blank">http://matita.cs.unibo.it/PAPERS/plmms09.pdf</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. "A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions" Logical Methods in Computer Science, V.8, n. 1 <a href="http://www.lmcs-online.org/ojs/viewarticle.php?id=960" target="_blank">http://www.lmcs-online.org/ojs/viewarticle.php?id=960</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> <li id="fn:5"><p>Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. "Hints in unification": LNCS V.5674, 2009, pp 84-98 <a href="https://link.springer.com/chapter/10.1007%2F978-3-642-03359-9_8" target="_blank">https://link.springer.com/chapter/10.1007%2F978-3-642-03359-9_8</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li> <li id="fn:6"><p>Claudio Sacerdoti Coen, Stefano Zacchiroli "Efficient Ambiguous Parsing of Mathematical Formulae" LNCS V.3119, 2004, pp 347-362 <a href="https://link.springer.com/chapter/10.1007%2F978-3-540-27818-4_25" target="_blank">https://link.springer.com/chapter/10.1007%2F978-3-540-27818-4_25</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li> <li id="fn:7"><p>Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli "Tinycals: Step by Step Tacticals" ENTCS V.174, n.2, 2007, Pages 125–142 <a href="http://www.sciencedirect.com/science/article/pii/S1571066107001740" target="_blank">http://www.sciencedirect.com/science/article/pii/S1571066107001740</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></p></li> <li id="fn:8"><p>Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen "Matita Tutorial" Journal of Formalized Reasoning, V.7, n. 2, 2014, Pages 91-199 <a href="http://jfr.unibo.it/article/view/4651" target="_blank">http://jfr.unibo.it/article/view/4651</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></p></li> </ol>