Matita is a proof assistant characterised by a rich, user extensible, output facility based on a widget for the rendering of MathML Presentation, and by the automatic handling of overloading by means of a flexible disambiguation mechanism. We show how to use these features to obtain a simple learning environment for natural deduction, without modifying the source code or Matita.
Natural Deduction Environment for Matita / SACERDOTI COEN, Claudio; Tassi, Enrico. - STAMPA. - 5625:(2009), pp. 486-491. (Intervento presentato al convegno 8th International Conference on Mathematical Knowledge Management (MKM 09) tenutosi a Grand Bend, Canada nel 10-12/07/2009).
Natural Deduction Environment for Matita
SACERDOTI COEN, CLAUDIO;TASSI, ENRICO
2009
Abstract
Matita is a proof assistant characterised by a rich, user extensible, output facility based on a widget for the rendering of MathML Presentation, and by the automatic handling of overloading by means of a flexible disambiguation mechanism. We show how to use these features to obtain a simple learning environment for natural deduction, without modifying the source code or Matita.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
