Proof Structures: Proofs as Formal Objects and as Data Structures

拟议的项目属于自动推理领域，这是人工智能的一个中心子领域，其主题是通过计算机进行推理的研究。典型的自动推理系统创建证明结构：证明的表示，组合演绎步骤，作为数据结构。证明结构一方面可以理解为以特定方式与逻辑公式相关的形式对象，另一方面可以理解为具体化这些形式对象并可用于实际应用的数据对象。该项目从这个意义上的证明结构的研究出发，旨在提高自动推理系统寻找证明的能力，并扩展它们可以解决的任务范围，超出严格意义上的定理证明。除了自动推理领域的理论和实验方法的相互作用之外，该项目的一个具体的系统方面是对给定证明的分析。特别相关的是，在计算机广泛使用之前，文献中有大量先进的正式证明，这些证明仍然不能通过自动化方法以令人满意的方式找到。该项目的具体目标是：(1)提高一阶定理证明者寻找证明的能力，特别是通过新颖的演算，通过从证明结构的方向产生的抽象和在证明分析中的观察来指导。(2)理论上理解和实现各种实际应用的证明转换，如缩短或简化证明，发现和抽象证明中的重复和规律，或演算之间的映射以实现不同系统的组合。(3)自动推理在整合数据和知识库的查询重构以及查询优化中的适用性。计划改进和扩展一种基于克雷格插值的查询重构方法，这是一阶逻辑中证明结构和相关公式之间的基本关系。(4)在与项目所考虑的核心技术、克雷格插值和凝聚分离相关的理论和实践兴趣的某些高级问题上取得进展。后者是所分析文献中的主要证明表示。目标是克服已知的限制，洞察与进一步技术的关系，以及进一步应用可能性的可用性。

The proposed project is in the area of automated reasoning, a central subfield of Artificial Intelligence, whose topic is the investigation of reasoning by means of the computer. Typical automated reasoning systems create proof structures: representations of proofs, combined deduction steps, as data structures. Proof structures can be understood on the one hand as formal objects that are related in specific ways to logical formulas, and, on the other hand, as data objects that materialize these formal objects and can be used for practical applications. Starting out from the investigation of proof structures in this sense, the project aims at both, improving the capability of automated reasoning systems to find proofs, and extending the range of tasks that can be solved by them, beyond theorem proving in the strict sense.Aside of the interplay of theoretical and experimental methods that characterizes the field of automated reasoning, a specific methodical aspect of the project is the analysis of given proofs. Of particular relevance is there an extensive corpus of advanced formal proofs from the literature before the broad availability of computers, which still can not be found in a satisfactory way by automated methods.The specific objectives of the project are: (1) Improving the capability of first-order theorem provers to find proofs, in particular through novel calculi, guided by abstractions emerging from the orientation at proof structures and by observations made in the analysis of proofs. (2) Theoretically well-understood and implemented proof transformations for various practical applications, such as shortening or simplification of proofs, discovery and abstraction of repetitions and regularities in proofs, or mappings between calculi to enable the combination of different systems. (3) Applicability of automated reasoning to query reformulation for integrating data and knowledge bases as well as query optimization. It is planned to refine and extend an approach to query reformulation that is based on Craig interpolation, a fundamental relationship in first-order logic between proof structures and associated formulas. (4) Progress in certain advanced issues of theoretical and practical interest that are related to the core techniques considered in the project, Craig interpolation and condensed detachment. The latter is the primary proof representation in the analyzed literature. Goals are in particular the overcoming of known limitations, insights into relationships to further techniques, and availability of further application possibilities.