权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Developing an intuitive automated theorem prover

开发直观的自动化定理证明器

基本信息

批准号：
1804138
负责人：
金额：
--
依托单位：
University of Cambridge
依托单位国家：
英国
项目类别：
Studentship
财政年份：
2016
资助国家：
英国
起止时间：
2016 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=studentship-1804138
关键词：
Developing 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.

与Tim Gowers教授(组合学)合作，作为坎塔布资本信息数学研究所的一部分。数学专家很少使用Proof助手和自动推理工具，通常是作为最后的手段。这个项目旨在探索如何改进这些工具，使其对数学家更具吸引力。我们打算通过构建系统来实现这一点，这些系统使用网络技术以人类的方式进行推理。这样做的目的是，这款网络应用程序将能够解释它是如何得出给定证据的，因此，这一应用的第一批可能会作为本科生的教学辅助工具。总而言之，我想开发一些系统，帮助克服这个可用性问题，并使自动定理证明器更好地为数学家工作。为了实现我开发一个直观的自动定理证明器的目标，我需要完成以下任务：1.将数学知识转换为易于计算的形式。这可以通过手动输入或对现有文本进行语言分析来实现，如[2].2所示。从已有的形式证明中综合自然语言证明。开发用于证明定理的逻辑和启发式方法，以模仿人类证明定理的方式。创建允许非专业用户直观地操作给定系统的用户界面。我对上述所有问题都感兴趣，但范围太大，不能作为博士项目来承担。在产生理论结果方面，我将主要关注(3)。但我也将实施(1)和(2)的现有研究，以及制作用户界面。