SHF: Small: WLoS: Without Loss of Satisfaction

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

基本信息

批准号：
2015445
负责人：
Marienus Heule
金额：
$ 50万
依托单位：
Carnegie-Mellon University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2019
资助国家：
美国
起止时间：
2019-11-02 至 2024-02-29
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2015445&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的法规使命，并认为通过基金会的知识优点和广泛的crietia crietia crietia crietia crietia criter criter criteria crietia criter criteria crietia criter criteria crietia crietia crietia crietia crietia crietia crietia crietia crietia cromitia criteria crietia均值得一提。

项目成果

期刊论文数量（15）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

SAT-Inspired Eliminations for Superposition

受 SAT 启发的叠加消除法

DOI：
10.34727/2021/isbn.978-3-85448-046-4_32
发表时间：
2021
期刊：
Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
影响因子：
0
作者：
Vukmirovic, Petar;Blanchette, Jasmin;Heule, Marijn
通讯作者：
Heule, Marijn

The Packing Chromatic Number of the Infinite Square Grid is 15

无限方格的堆积色数为15

DOI：
发表时间：
2023
期刊：
Springer
影响因子：
0
作者：
Subercaseaux, Bernardo;Heule, Marijn J.
通讯作者：
Heule, Marijn J.

Leibniz International Proceedings in Informatics (LIPIcs):14th Innovations in Theoretical Computer Science Conference (ITCS 2023)

莱布尼茨国际信息学会议录 (LIPIcs)：第 14 届理论计算机科学创新会议 (ITCS 2023)

DOI：
10.4230/lipics.itcs.2023.101
发表时间：
2023
期刊：
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
影响因子：
0
作者：
Yolcu, Emre;Heule, Marijn J.
通讯作者：
Heule, Marijn J.

Compact Symmetry Breaking for Tournaments

锦标赛的紧凑对称破缺

DOI：
发表时间：
2022
期刊：
Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022
影响因子：
0
作者：
Lohn, Evan;Lambert, Chris;Heule, Marijn J.
通讯作者：
Heule, Marijn J.

What's in a Name? Linear Temporal Logic Literally Represents Time Lines

名字里有什么？

DOI：
10.1109/vissoft60811.2023.00018
发表时间：
2023
期刊：
IEEE
影响因子：
0
作者：
Li, Runming;Gurushankar, Keerthana;Heule, Marijn J.H.;Rozier, Kristin Yvonne
通讯作者：
Rozier, Kristin Yvonne