- <p class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-matita.png">
- <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
- </a>
- </span>
-
- Matita e' basato sul Calcolo delle Costruzioni (Co)Induttive, ed
- parzialmente compatibile con l'analogo strumento francese
- <a href="http://coq.inria.fr">Coq</a>.
- Matita e' una applicazione ragionevolmente semplice e piccola,
- la cui complessita' architetturale puo' essere
- padroneggiata da laureandi, facendone uno strumento particolarmente
- utile per la sperimentazione di nuove idee e soluzioni in ambito
- universitario.
- Matita adotta una filosofia di scrittura delle prove basata su
- tattiche; lambda-termini di prova (codificati in XML) sono prodotti
- per la memorizzazione di lungo periodo e lo scambio di dati
- con altri sistemi.
- </p>
-
- <p class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-matita-href.png">
- <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
- </a>
- <a class="quiet" href="images/screenshot-matita-selection.png">
- <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
- </a>
- </span>
- L'interfaccia grafica e' stata ispirata da CtCoq e
- <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
- Supporta una resa bidimensionale di alta qualita' delle espressioni
- basata sul markup
- <a href="http://www.w3.org/Math/">MathML</a>.</p>