Name
Abstract | ||
|---|---|---|
The Mizar proof language has both many human-friendly presentation features, and also firm semantical level allowing rigorous proof checking. Both the presentation features and the semantics are important for users, and an ideal Mizar presentation should be both human-friendly (i.e. very close to textbook presentations), and also allowing fast access to the detailed semantics and detailed proof explanations. This poses several questions, problems and choices when presenting original Mizar texts, presenting results of semantic queries over the Mizar library, and also when presenting texts produced directly on the semantical level, e.g. by automated theorem provers. This paper discusses solutions to these problems, and particularly implements an initial system for presenting detailed explanations of atomic Mizar inferences. This is done by the cooperation of the Mizar XML presentation tools, the MML Query system, and automated theorem provers working on the MPTP semantic translation of Mizar. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1016/j.entcs.2006.09.022 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
mizar xml presentation tool,mptp,proof presentation,presentation feature,atp,detailed explanation,mml query,mizar,human-friendly presentation feature,proof objects,textbook presentation,mizar library,atomic mizar inference,mizar proof language,ideal mizar presentation,original mizar text,theorem prover | Mizar system,Proof checking,XML,Computer science,Automated proof checking,Theoretical computer science,Automated theorem provers,Semantic translation,Semantics | Journal |
Volume | Issue | ISSN |
174 | 2 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
5 | 0.48 | 14 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Josef Urban | 1 | 102 | 12.92 |
| Grzegorz Bancerek | 2 | 96 | 19.74 |