|
Matita〔 Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi. "The Matita Interactive Theorem Prover": ( CADE-23, LNCS 6803, 2011, pp. 64-69 ). 〕 is an experimental proof assistant under development at the Computer Science Department of the University of Bologna. It is a tool aiding the development of formal proofs by man-machine collaboration, providing a programming environment where formal specifications, executable algorithms and automatically verifiable correctness certificates naturally coexist. Matita is based on a Dependent Type System known as the Calculus of (Co)Inductive Constructions (a derivative of Calculus of Constructions), and is compatible, to some extent, with Coq. The word matita means "pencil" in Italian (a simple and widespread editing tool). It is a reasonably small and simple application,〔 Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. "A compact kernel for the calculus of inductive constructions": (Sadhana 2009, V.34,n.1, pp 71-144 ) 〕 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. ==Main features== Existential variables are native in Matita, allowing a simpler management of dependent goals.〔 Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. "A new type for tactcis": (Technical Report UBLCS-2009-14. June 2009. ) 〕 Matita implements a bidirectional type inference algorithm〔 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,n1 ) 〕 exploiting both inferred and expected types. The power of the type inference system (refiner) is further augmented by a mechanism of hints〔 Andrea Asperti, Wilmer Ricciotti, C Sacerdoti Coen, Enrico Tassi. "Hints in unification": (LNCS V.5674, 2009, pp 84-98 ) 〕 that helps in synthetizing unifiers in particular situations specified by the user. Matita supports a sophisiticated disambiguation strategy〔 Claudio Sacerdoti Coen, Stefano Zacchiroli "Efficient Ambiguous Parsing of Mathematical Formulae" (LNCS V.3119, 2004, pp 347-362 ) 〕 based on a dialog between the parser and the typechecker. At the interactive level, the system implements a small step execution of structured tactics〔 Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli "Tinycals: Step by Step Tacticals" (ENTCS V.174, n.2, 2007, Pages 125–142 ) 〕 allowing a much better management of the proof development, and naturally leading to more structured and readable scripts. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Matita」の詳細全文を読む スポンサード リンク
|