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