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.