SHF: Small: WLoS: Without Loss of Satisfaction

SHF：小：WLoS：不丧失满意度

• 批准号: 1910438
• 负责人: Marienus Heule
• 金额: $ 50万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-11-01 至 2020-02-29
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1910438&HistoricalAwards=false
• 关键词: SHF; Small; WLoS; Without; Loss

The key to automating activities that are traditionally performed by humans, such as assembly-line work or organizational tasks, is to break these activities down into numerous simple steps that can be handled easily. While this approach has also been used to automate logical reasoning, breaking reasoning tasks into overly simple steps has two important shortcomings. First, it can prevent today's methods from solving some seemingly easy problems. Second, a long sequence of these simple steps is often impossible to understand for humans. This project explores a novel approach to automated reasoning that deals with this issue by allowing more elaborate, but also understandable, steps.Over half a century, research regarding reasoning systems has centered on the existence of short arguments that could in theory be found by computers, without addressing the issue of how to actually find these arguments in practice. The novel reasoning systems studied in this project aim at automatically finding arguments that are usually used by mathematicians, in particular arguments "without loss of generality," which can be automated efficiently. The main goals of the research are (1) solving problems that are too hard for existing reasoning techniques, (2) producing short arguments for problems for which we only have gigantic arguments, and (3) learning from the results of automated reasoning.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

自动化传统上由人工执行的活动(如装配线工作或组织任务)的关键是将这些活动分解为许多易于处理的简单步骤。虽然这种方法也被用于自动化逻辑推理，但将推理任务分解为过于简单的步骤有两个重要的缺点。首先，它可以阻止今天的方法解决一些看似容易的问题。其次，这些简单步骤的一长串对人类来说往往是不可能理解的。这个项目探索了一种新的自动化推理方法，通过允许更详细但也可以理解的步骤来处理这个问题。半个世纪以来，关于推理系统的研究一直集中在理论上可以由计算机找到的简短论点的存在上，而没有解决如何在实践中实际找到这些论点的问题。这个项目中研究的新型推理系统旨在自动找到数学家通常使用的论点，特别是可以高效地自动执行的“不失一般性”的论点。这项研究的主要目标是(1)解决对现有推理技术来说太难的问题，(2)为我们只有巨大争论的问题产生简短的论点，以及(3)从自动推理的结果中学习。这一奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。