Information Retrieval and Rendering with MML Query

摘要

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.