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

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

• 批准号: 0957438
• 负责人: Geoffrey Sutcliffe
• 金额: $ 1.58万
• 依托单位: University of Miami
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-05-01 至 2012-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0957438&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.

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