作　　者： ; ;

机构地区： 武汉大学计算机学院计算机科学系

出　　处： 《武汉大学学报（自然科学版）》 1996年第1期55-62,共8页

摘　　要： 以计算逻辑为基础,介绍了定理机器证明中一种新的启发式方法——波动方法,它是一种在证明中通过处理归纳结论来激活归纳假设的策略。 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.

关 键 词： 定理机器证明 波动 波前 繁殖 计算逻辑

领　　域： [自动化与计算机技术] [自动化与计算机技术]