图表追踪的一种机器实现方法

交换图表追踪法是同调代数中一种重要的证明方法.本文提出了一种基于前推的交换图表追踪的机器实现方法,它可以证明同调代数中一系列基于交换图的定理.该方法从定理的结论出发,通过构造辅助元素以及对辅助元素进行推导,能在有限步内给出定理的证明.本文提出的前推方法已经在Java开发平台上实现,同调代数中的五引理、九引理、蛇引理等的证明都可以由我们的程序自动产生.

A method for mechanically diagram chasing

Diagram chasing is an important proof method used in homological algebra. In this paper, we present a method based on forward chaining for automated generation of proofs for homological theorems involving commutative diagrams. First, auxiliary elements are constructed according to the conclusion. Then we do forward chaining to these elements with a set of rewrite rules until the desired elements or results are constructed or verified. The algorithm given in this paper has been implemented in Java development platform and our experiments show that the method can prove many theorems, including the Five Lemma, the Nine Lemma and the Snake Lemma.