Combining Mizar and TPTP Semantic Presentation Tools
Abstract:
This paper describes a combination of several Mizar-based tools (the MPTP trans-
lator, XSL style sheets for Mizar), and TPTP-based tools (IDV, AGInT, Syste-
mOnTPTP) used for visualizing and analyzing Mizar proofs. The combination de-
livers to the readers of the Mizar Mathematical Library (MML) an easy, powerful,
and almost playful way of exploring the semantics and the structure of the library.
The key factors for the relative easiness of having these functionalities are the choice
of XML as both internal and external interface of Mizar, and the existence of a TPTP
representation of MML articles. This clearly shows the great added value that can be
obtained by cooperation of several quite diverse (and quite often separately developed)
projects, provided that they are based on the same communication standards.