Proof Structures: Proofs as Formal Objects and as Data Structures

证明结构：作为形式对象和数据结构的证明

• 批准号: 457292495
• 负责人: Dr. Christoph Wernhard
• 金额: --
• 依托单位: Institut für Informatik und Computational Science
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/457292495?language=en
• 关键词: Proof; Structures; Proofs; Formal; Objects

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.

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