计算逻辑中的波动策略

计算逻辑中的波动策略 RIPPLING-OUT TACTIC FOR A COMPUTATIONAL LOGIC 印鉴 Yin Jian 1 2 3 first-author 张黔 Zhang Qian 1 2 3 武汉大学计算机科学系 武汉大学计算机科学系 Department of Computer Science, Wuhan University Department of Computer Science, Wuhan University 武汉大学计算机科学系,武汉 武汉大学计算机科学系,武汉 ,430072 ,430072 以计算逻辑为基础,介绍了定理机器证明中一种新的启发式方法——波动方法,它是一种在证明中通过处理归纳结论来激活归纳假设的策略。 Based on a computational logic, this paper introduces a new heuristic approach called rippling-out tactic in mechanical theorem proving. It is a tactic for manipulating the induction conclusion to enable the induction hypothesis to be used in its proof. 定理机器证明 波动 波前 繁殖 聚元 汇点 mechanical theorem proving rippling-out wave front fertilization accumulator sink TP301 1996-01-01 2021-04-01 1