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

University Of Miami, Coral Gables FL

Investigators

Abstract

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.