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

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

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.