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

• 作者: 叶征 李洪波 谢正 黄雷
• 来源期刊: 中国科学A辑
• 关键词: 自动定理证明 同调代数 交换图 图表追踪 前推
• 年，卷（期）: 2010,（7）
• 所属期刊栏目: 论文
• 页码范围: 661-672
• 页数: 12页
• 语种: 中文

摘要

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