CRI: CRD Libraries and Software for Automated Deduction

University Of New Mexico, Albuquerque NM

Investigators

Abstract

This project is to design, develop, and disseminate software infrastructure to support research and education in automated deduction and formal methods. The core of the infrastructure will be software for high-performance first-order methods. It will include libraries of modules for construction special-purpose deduction systems as well as stand-alone programs that search for proofs and for counterexamples. The work will be easily accessible, and it will be emphasize documentation of the ifrastructure in the form of application programmer interfaces, manuals, tutorials, and examples. Intellectual Merit. Design and development of the software will lead to a better understanding of high-performance implementation and integration of complex deduction algorithms. By facilitating the construction of experimental deduction software, the infrastructure will lead to a deeper understanding of (1) search strategies and heuristics for difficult conjectures, (2) the differences in proof structure between proofs found by humans and those found by computers, and (3) ways of combining disparate deduction methods. The infrastructure will enable new applications of automated deduction to difficult problems in mathematics and logic, leading to new results in those areas. It will lead to better understanding of the application of formal methods to computer and information systems. Broader Impacts. The result will be a resource for a wide community of researchers and educators. Researchers in automated deduction methods will be able to easily construct prototype programs for experimentation with new methods. Researchers in formal methods will be able to use the software libraries to study combination methods and to build high-performance verification systems. Information engineers will be able to experiment with the relationshops between problem representations and search methods.