Integrating Searching and Authoring in Mizar

13 years 5 months ago
Integrating Searching and Authoring in Mizar
The vision of a computerised assistant to mathematicians has existed since the inception of theorem proving systems. The Alcor system has been designed to investigate and explore how a mathematician might interact with such an assistant by providing an interface to Mizar and the Mizar Mathematical Library. Our current research focuses on the integration of searching and authoring while proving. In this use a scenario to elaborate the nature of the interaction. We abstract from the scenario two distinct styles of searching and describe how the Alcor interface implements these with keyword and LSI-based search. Though Alcor is still in its early stages of development, there are clear implications for the general problem of integrating searching and authoring, as well as technical issues with Mizar.
Paul A. Cairns, Jeremy Gow
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where JAR
Authors Paul A. Cairns, Jeremy Gow
Comments (0)