Collaborative Research: CI-ADDO-NEW: *-EXEC: A Cross-Community Solver Execution Service

协作研究：CI-ADDO-NEW：*-EXEC：跨社区求解器执行服务

• 批准号: 0958160
• 负责人: Aaron Stump
• 金额: $ 8.42万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-05-01 至 2012-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0958160&HistoricalAwards=false
• 关键词: Collaborative; Research; CI; ADDO; NEW

Ongoing breakthroughs in nationally important research areas like Verification and Artificial Intelligence depend on continuing advances in high-performance automated theorem proving tools. The typical use of these tools is as backends: application problems are translated by an application tool into (typically very large and complex) logic formulas, which are then handed off to a logic solver. Different tradeoffs between linguistic expressiveness and the difficulty of solving the resulting problems give rise to different logics. Solver communities, formed around these different logics, have developed their own community research infrastructures to encourage innovation and ease adoption of their solver technology. Such infrastructure includes standard formats for logic formulas, libraries of benchmark formulas, and regular solver competitions to spur solver advances.Currently, these different infrastructures are all developed separately, at significant cost in equipment and support. These costs are paid again and again for the different services, since there is currently no global piece of computing infrastructure suitable for the logic solving domain, which all these communities can use. This project is building a simplified proof-of-concept of a single piece of shared computing infrastructure, which could eventually be used by many different logic solver communities. The award also provides other support for soliciting research community feedback on the prototype and the design of a comprehensive infrastructure.

验证和人工智能等国家重要研究领域的持续突破依赖于高性能自动化定理证明工具的持续进步。这些工具的典型用途是作为后端：应用程序问题通过应用程序工具转换为（通常非常大且复杂的）逻辑公式，然后将其传递给逻辑求解器。不同的语言表达能力和解决问题的难度之间的权衡产生了不同的逻辑。围绕这些不同的逻辑形成的求解器社区已经开发了自己的社区研究基础设施，以鼓励创新并简化其求解器技术的采用。这些基础设施包括逻辑公式的标准格式、基准公式库和定期求解器竞赛，以促进求解器的进步。目前，这些不同的基础设施都是单独开发的，设备和支持成本很高。这些成本是为不同的服务一次又一次地支付的，因为目前还没有适合逻辑解决领域的全局计算基础设施，所有这些社区都可以使用。该项目正在构建单个共享计算基础设施的简化概念验证，它最终可以被许多不同的逻辑求解器社区使用。该奖项还为征求研究社区对原型和综合基础设施设计的反馈提供其他支持。