TY - JOUR

T1 - Identification of proofs via syzygies

AU - Malheiro, António

AU - Reis, José Francisco

N1 - info:eu-repo/grantAgreement/FCT/5876/147204/PT#
For both authors, this work was partially supported by the Fundacao para a Ciencia e a Tecnologia (Portuguese Foundation for Science and Technology) through the project UID/MAT/00297/2013 (Centro de Matematica e Aplicacoes) and the project PTDC/MHC-FIL/2583/2014. The first author was also funded by the FCT project PTDC/MAT-PUR/31174/2017.

PY - 2019/3/11

Y1 - 2019/3/11

N2 - 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.

AB - 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.

KW - Hilbert’s 24th problem

KW - Identification of proofs

KW - Syzygies

UR - http://www.scopus.com/inward/record.url?scp=85061315416&partnerID=8YFLogxK

U2 - 10.1098/rsta.2018.0275

DO - 10.1098/rsta.2018.0275

M3 - Article

C2 - 30966976

AN - SCOPUS:85061315416

VL - 377

JO - Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences

JF - Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences

SN - 1364-503X

IS - 2140(SI)

M1 - Y

ER -