关键词: 相干逻辑 自动推理 演绎 可读证明 证明树

Abstract:

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.

Key words: relevance logic, automated reasoning, deduction, readable proof, reasoning tree