User interaction with the matita proof assistant

被引：35

作者：

Asperti, Andrea ^{[1
]}

Coen, Claudio Sacerdoti ^{[1
]}

Tassi, Enrico ^{[1
]}

Zacchiroli, Stefano ^{[1
]}

机构：

[1] Univ Bologna, Dept Comp Sci, I-40127 Bologna, Italy

来源：

JOURNAL OF AUTOMATED REASONING | 2007年 / 39卷 / 02期

关键词：

proof assistant; interactive theorem proving; digital libraries; XML; mathematical knowledge management; authoring;

D O I：

10.1007/s10817-007-9070-5

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Matita is a new, document-centric, tactic-based interactive theorem prover. This paper focuses on some of the distinctive features of the user interaction with Matita, characterized mostly by the organization of the library as a searchable knowledge base, the emphasis on a high-quality notational rendering, and the complex interplay between syntax, presentation, and semantics.

引用

页码：109 / 139

页数：31

共 37 条

[1] Interactive theorem proving: An empirical study of user activity [J].

Aitken, JS ;

Gray, P ;

Melham, T ;

Thomas, M .

JOURNAL OF SYMBOLIC COMPUTATION, 1998, 25 (02) :263-284

[2]

AITKEN S, 1996, EUR C ART INT ECAI, P335

[3] Mathematical knowledge management in HELM [J].

Asperti, A ;

Padovani, L ;

Coen, CS ;

Guidi, F ;

Schena, I .

ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2003, 38 (1-3) :27-46

[4]

ASPERTI A, 2000, 15 IEEE S LOG COMP S

[5]

ASPERTI A, 2003, LNCS, V2730, P14

[6]

ASPERTI A, 2001, P EXTREME MARK LANG

[7]

Asperti ] A., 2004, LNCS, V3839, P17, DOI DOI 10.1007/11617990_2

[8]

Aspinall D, 2000, LNCS, V1785

[9]

BANCEREK G, 2003, LNCS, V2594

[10]

BANCEREK G, 2003, ELECT NOTES THEOR CO, V85

← 1 2 3 4 →