Information retrieval and rendering with MML Query

G Bancerek - International Conference on Mathematical Knowledge …, 2006 - Springer
G Bancerek
International Conference on Mathematical Knowledge Management, 2006Springer
Mizar, a proof-checking system, is used to build the Mizar Mathematical Library (MML). MML
Query is a semantics-based tool for managing the mathematical knowledge in Mizar
including searching, browsing and presentation of the evolving MML content. The tool is
becoming widely used as an aid for Mizar authors and plays an essential role in the ongoing
reorganization of MML. We present new features of MML Query implemented in the third
release and describe the possibilities offered by them.
Abstract
Mizar, a proof-checking system, is used to build the Mizar Mathematical Library (MML). MML Query is a semantics-based tool for managing the mathematical knowledge in Mizar including searching, browsing and presentation of the evolving MML content. The tool is becoming widely used as an aid for Mizar authors and plays an essential role in the ongoing reorganization of MML. We present new features of MML Query implemented in the third release and describe the possibilities offered by them.
Springer