CRI: CRD Libraries and Software for Automated Deduction

该项目旨在设计、开发和传播软件基础设施，以支持自动演绎和形式化方法方面的研究和教育。基础设施的核心将是高性能一阶方法的软件。它将包括用于构建特殊用途演绎系统的模板库，以及搜索证据和反例的独立程序。这项工作将很容易获得，它将是以应用程序编程人员界面、手册、教程和示例的形式强调基础设施结构的文档。软件的设计和开发将有助于更好地理解复杂演绎算法的高性能实现和集成。通过促进实验演绎软件的建设，该基础设施将导致对(1)困难猜想的搜索策略和启发式方法，(2)人类发现的证明与计算机发现的证明结构的差异，以及(3)结合不同演绎方法的方法的更深入的理解。该基础设施将使自动演绎能够对数学和逻辑中的难题进行新的应用，从而在这些领域产生新的结果。它将有助于更好地理解形式化方法在计算机和信息系统中的应用。其结果将成为广大研究人员和教育工作者的资源。自动演绎方法的研究人员将能够轻松地构建原型程序，用于使用新方法进行实验。正式方法的研究人员将能够使用软件库来研究组合方法并建立高性能的验证系统。信息工程师将能够试验问题表示和搜索方法之间的关系。

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.