caa a22 4500 463182979 CHVBK 20180406164844.0 cr unu---uuuuu 170326e20070801xx s 000 0 eng 10.1007/s10817-007-9073-2 doi (NATIONALLICENCE)springer-10.1007/s10817-007-9073-2 Integrating Searching and Authoring in Mizar [Elektronische Daten] [Paul Cairns, Jeremy Gow] The vision of a computerized 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 paper we use a scenario to elaborate on the nature of the interaction. We abstract from the scenario two distinct styles of searching and describe how the Alcor interface implements these with a 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. Springer Science+Business Media, Inc., 2007 LSI nationallicence Alcor nationallicence Mizar nationallicence Information retrieval nationallicence Mathematics nationallicence Cairns Paul UCL Interaction Centre, University College London, 31-32 Alfred Place, WC1E 7DP, London, UK aut Gow Jeremy UCL Interaction Centre, University College London, 31-32 Alfred Place, WC1E 7DP, London, UK aut Journal of Automated Reasoning Springer Netherlands 39/2(2007-08-01), 141-160 0168-7433 39:2<141 2007 39 10817 https://doi.org/10.1007/s10817-007-9073-2 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-007-9073-2 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Cairns Paul UCL Interaction Centre, University College London, 31-32 Alfred Place, WC1E 7DP, London, UK aut NATIONALLICENCE 700 1- Gow Jeremy UCL Interaction Centre, University College London, 31-32 Alfred Place, WC1E 7DP, London, UK aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Springer Netherlands 39/2(2007-08-01), 141-160 0168-7433 39:2<141 2007 39 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer