Suppr超能文献

通过合冲来识别证据。

Identification of proofs via syzygies.

机构信息

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.

Abstract

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 个问题”的一部分。

相似文献

1
Identification of proofs via syzygies.通过合冲来识别证据。
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180275. doi: 10.1098/rsta.2018.0275.
4
Proof simplification and automated theorem proving.证明简化与自动定理证明。
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180034. doi: 10.1098/rsta.2018.0034.
5
Visual thinking and simplicity of proof.视觉思维与证明的简洁性。
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180032. doi: 10.1098/rsta.2018.0032.
6
The Cantor-Bernstein theorem: how many proofs?坎托-伯恩斯坦定理:有多少种证明?
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180031. doi: 10.1098/rsta.2018.0031.
7
Prolegomena to any theory of proof simplicity.证明简约性理论的绪论。
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180035. doi: 10.1098/rsta.2018.0035.
8
Explanation in mathematical conversations: an empirical investigation.数学对话中的解释:一项实证研究。
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180159. doi: 10.1098/rsta.2018.0159.
9
Reshaping the metaphor of proof.重塑证据的隐喻。
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180279. doi: 10.1098/rsta.2018.0279.

引用本文的文献

1
Discussing Hilbert's 24th problem.讨论希尔伯特的第24个问题。
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180040. doi: 10.1098/rsta.2018.0040.

文献检索

告别复杂PubMed语法,用中文像聊天一样搜索,搜遍4000万医学文献。AI智能推荐,让科研检索更轻松。

立即免费搜索

文件翻译

保留排版,准确专业,支持PDF/Word/PPT等文件格式,支持 12+语言互译。

免费翻译文档

深度研究

AI帮你快速写综述,25分钟生成高质量综述,智能提取关键信息,辅助科研写作。

立即免费体验