CI-EN: SystemOnTPTP - Online Services for Automated Theorem Proving in Classical Logic

自动定理证明（Automated Theorem Proving， ATP）关注的是自动化合理推理系统的开发和使用：从事实中不可避免地推导出结论。这种能力是许多重要计算任务的核心，例如，软件和硬件设计和验证的形式化方法，网络安全协议的分析，数学难题的解决，社会系统的分析，语义网的推理等。尽管ATP的使用越来越多，但在逻辑中准备问题，安装和执行适当的ATP系统以及从ATP系统输出中提取有用信息的复杂性通常是使用ATP的障碍。软件基础设施已经为社区提供了近十年，通过为经典逻辑的ATP提供在线服务，克服了这些障碍。NSF CRI项目将帮助升级承载该基础设施的硬件。该系统有三个组成部分：首先，它提供准备ATP问题的工具，然后提供用于解决ATP问题的服务，最后服务提供分析输出和解决方案的工具。所有这三个组件都可以通过面向人类的交互式web界面和应用程序编程接口获得。硬件包括一个用于构建和测试ATP系统和工具的服务器，以及一个用于服务用户请求的计算服务器。硬件升级将使系统能够继续提供最新版本的ATP系统和工具，同时保持必要的性能和响应水平。

Automated Theorem Proving (ATP) is concerned with the development and use of systems that automate sound reasoning: the derivation of conclusions that follow inevitably from facts. This capability lies at the heart of many important computational tasks, e.g., formal methods for software and hardware design and verification, the analysis of network security protocols, solving hard problems in mathematics, analysis of social systems, inference for the semantic web etc. Despite increased usage of ATP, the complexities of preparing problems in a logic, installing and executing appropriate ATP systems, and extracting useful information from the ATP system's output often present a barrier to using ATP. The software infrastructure, which have been available to the community for almost a decade now, overcomes these barriers by providing online services for ATP in classical logic. The NSF CRI program will help to upgrade the hardware that hosts this infrastructure. The system has three components: first, it provides tools for preparing ATP problems, it then provides services that are used to solve ATP problems, and finally the service provides tools for analyzing the output and the solutions. All three components are available through interactive web interfaces for humans, and application programming interfaces. The hardware consists of a server used for building and testing ATP systems and tools before they are made available, and a compute server used to service requests from users. The hardware upgrade will make it possible for the system to continue to offer the most recent versions of ATP systems and tools, while maintaining the necessary performance and response levels.