Developing an intuitive automated theorem prover

点击翻译按钮获取中文摘要

Working with Prof Tim Gowers (Combinatorics) as part of the Cantab Capital Institute for the Mathematics of Information.Proof assistants and automated reasoning tools are used sparingly by mathematicians, and usually as a last resort. This project aims to explore how these tools could be improved to make them more appealing to mathematicians. We intend to achieve this by building systems which reason in a human-like way using web technologies. The aim is that this web-app will be able explain how it arrived at a given proof, so the first applications of this are likely to be useful as a teaching aid to undergraduates. In broad terms, I want to develop systems which help to overcome this usability problem and make automated theorem provers work better for mathematicians. To achieve my aim of developing an intuitive automated theorem prover, I will need to complete the following tasks:1. Translation of mathematical knowledge to an easily computable form. This can be achieved either through manual entry or linguistic analysis of existing texts as demonstrated in [2].2. Synthesis of natural language proofs from existing formal proofs.3. Developing logics and heuristics for proving theorems in a way that mimics how a human would prove theorems.4. Creating user interfaces which allow a non-specialist user to intuitively operate the given system.I am interested in all of the above problems, but the scope is too large to be undertaken as a PhD project. In terms of producing theoretical results, I will mainly concern myself with (3). But I will also be implementing existing research on (1) and (2) as well as producing user interfaces.