Natural Deduction Environment for Matita

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.

• Type: Conference
• Year: 2009
• Where: MKM
• Authors: Claudio Sacerdoti Coen, Enrico Tassi
• Keywords: Information Management, MKM 2009, Proof Assistant, Simple Learning Environment, flexible Disambiguation Mechanism