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.