摘要
提出针对重言衍推系统的模仿人类思维方式的生成可读证明的算法:试探法。试探法将待证的命题逐步分解成子命题并构造一颗证明树,对重言衍推系统中的定理证明取得了较好的效果。
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.
出处
《计算机应用与软件》
CSCD
2009年第9期34-37,45,共5页
Computer Applications and Software
基金
国家重点基础研究发展项目(2004CB318003)
国家自然科学基金重点项目(90718041)
关键词
重言衍推
自动推理
可读证明
证明树
试探法
Tautology entailment Automated reasoning Readable proofs Reasoning tree Heuristic algorithm
