Proof Structures: Proofs as Formal Objects and as Data Structures

拟议的项目是自动推理领域，这是人工智能的一个中心子领域，其主题是通过计算机进行推理的调查。典型的自动推理系统创建证明结构：证明的表示、组合演绎步骤，作为数据结构。证明结构一方面可以理解为以特定方式与逻辑公式相关的形式对象，另一方面可以理解为将这些形式对象具体化并可用于实际应用的数据对象。从这个意义上的证明结构的研究出发，该项目的目标是提高自动推理系统寻找证据的能力，并扩展它们可以解决的任务的范围，而不仅仅是严格意义上的定理证明。除了自动推理领域的理论和实验方法的相互作用之外，该项目的一个具体的方法论方面是对给定证明的分析。特别重要的是，在计算机广泛使用之前，有大量高级形式证明的文献语料库，这些高级形式证明仍然不能通过自动化方法以令人满意的方式找到。该项目的具体目标是：(1)提高一阶定理证明者发现证明的能力，特别是通过新颖的演算，在从证明结构的取向和在证明分析中所做的观察的指导下，提高一阶定理证明者发现证明的能力。(2)理论上理解并实现了各种实际应用的证明转换，如证明的缩短或简化，证明中重复和规则的发现和抽象，或演算之间的映射，以使不同的系统能够组合。(3)自动推理对查询重构、数据和知识库集成以及查询优化的适用性。计划改进和扩展一种基于Craig插值法的查询重构方法，Craig插值法是一阶逻辑中证明结构和相关公式之间的基本关系。(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.