重言衍推系统的试探法自动证明  

AUTOMATED PROVING OF HEURISTIC ALGORITHM FOR TAUTOLOGY ENTAILMENT SYSTEM

作　　者：郭远华[1] 曾振柄[1] 

机构地区：[1]华东师范大学软件学院,上海200062

出　　处：《计算机应用与软件》2009年第9期34-37,45,共5页Computer Applications and Software

基　　金：国家重点基础研究发展项目(2004CB318003);国家自然科学基金重点项目(90718041)

摘　　要：提出针对重言衍推系统的模仿人类思维方式的生成可读证明的算法:试探法。试探法将待证的命题逐步分解成子命题并构造一颗证明树,对重言衍推系统中的定理证明取得了较好的效果。This paper proposes a heuristic algorithm for tautology entailment system, which imitates human thinking mode and produces readable proofs. This algorithm gradually decomposes one proposition into one or two sub-propositions and constructs a reasoning tree, and is effective in proving theorems of tautology entailment system.

关 键 词：重言衍推 自动推理 可读证明 证明树 试探法 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术] TP301.6