摘要
本文提出了相干命题逻辑系统R的一种演绎生成算法——试探法。该算法采用后向推理法,依据推理规则将待证命题逐步分解成子命题并构造一棵证明树,对系统R中的定理证明取得了较好的效果。
This paper proposes a probing algorithm based on the deduction of the relevance propositional logic systemR. This algorithm adopts a backward method, gradually decomposes one proposition into one or two propositions, and constructs a reasoning tree, which is effective in proving the theorems of systemR.
出处
《计算机工程与科学》
CSCD
2008年第12期105-109,共5页
Computer Engineering & Science
基金
国家973计划资助项目(2004CB318003)
国家自然科学基金重点资助项目(90718041)
关键词
相干逻辑
自动推理
演绎
可读证明
证明树
relevance logic
automated reasoning
deduction
readable proof
reasoning tree
