1 Departamento de Matemática , Faculdade de Ciências e Tecnologia , Universidade Nova de Lisboa , 2829-516 Caparica , Portugal.
2 Centro de Matemática e Aplicações (CMA) , Faculdade de Ciências e Tecnologia , Universidade Nova de Lisboa , 2829-516 Caparica , Portugal.
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180275. doi: 10.1098/rsta.2018.0275.
In 1900, Hilbert gave a lecture at the International Congress of Mathematicians in Paris, for which he prepared 23 problems that mathematicians should solve during the twentieth century. It was found that there was a note on a 24th problem focusing on the problem of simplicity of proofs. One of the lines of research that was generated from this problem was the identification of proofs. In this article, we present a possible method for exploring the identification of proofs based on the membership problem original from the theory of polynomial rings. To show this, we start by giving a complete worked-out example of a membership problem, that is the problem of checking if a given polynomial belongs to an ideal generated by finitely many polynomials. This problem can be solved by considering Gröbner bases and the corresponding reductions. Each reduction is a simplification of the polynomial and it corresponds to a rewriting step. In proving that a polynomial is a member of an ideal, a rewriting process is used, and many different such processes can be considered. To better illustrate this, we consider a graph where each rewriting step corresponds to an edge, and thus a path corresponds to a rewriting process. In this paper, we consider the identification of paths, within the context of the membership problem, to propose a criterion of identification of proofs. This article is part of the theme issue 'The notion of 'simple proof' - Hilbert's 24th problem'.
1900 年，希尔伯特在巴黎举行的国际数学家大会上发表了演讲，为此他准备了 23 个问题，供 20 世纪的数学家解决。人们发现，在第 24 个问题上有一个注释，重点是证明的简单性问题。从这个问题中产生的一个研究方向是证明的识别。在本文中，我们提出了一种基于多项式环理论中的成员问题来探索证明识别的可能方法。为了说明这一点，我们首先给出了一个成员问题的完整实例，即检查一个给定的多项式是否属于由有限个多项式生成的理想的问题。这个问题可以通过考虑 Gröbner 基和相应的约简来解决。每个约简都是多项式的简化，对应于一个重写步骤。在证明一个多项式是一个理想的成员时，使用重写过程，并且可以考虑许多不同的这样的过程。为了更好地说明这一点，我们考虑一个图，其中每个重写步骤对应于一条边，因此一条路径对应于一个重写过程。在本文中，我们考虑在成员问题的上下文中识别路径，以提出证明的识别准则。本文是主题为“简单证明的概念——希尔伯特的第 24 个问题”的一部分。
