COMBINING MIZAR AND TPTP SEMANTIC PRESENTATION AND VERIFICATION TOOLS

• Authors: Urban Josef , Sutcliffe Geoff , Trac Steven , Puzis Yury
• Languages of publication: EN

Abstracts

EN

This paper describes a combination of several Mizar-based tools (the MPTP translator, XSL style sheets for Mizar), and TPTP-based tools (IDV, AGInT, SystemOnTPTP, GDV) used for visualizing, analyzing, and independent verication of Mizar proofs. The combination delivers 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 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.

Keywords

EN

MIZAR; SEMANTIC PRESENTATION; TPTP; VERIFICATION

Discipline

• LIBRARY_&_INFORMATION_SCIENCE: LIBRARY & INFORMATION SCIENCE

• Publisher: Sciendo
• Journal: Studies in Logic, Grammar and Rhetoric
• Year: 2009
• Issue: 18(31)
• Pages: 121-136
• Document type: ARTICLE

Contributors

author

Urban Josef

author

Sutcliffe Geoff

author

Trac Steven

author

Puzis Yury

• Josef Urban - Charles University, Czech Republic; Geoff Sutcliffe, Steven Trac, Yury Puzis - University of Miami, USA

Identifiers

CEJSH db identifier

11PLAAAA10169