启发式方法生成命题逻辑可读证明

Heuristic methods for generating readable proofs in propositional logic

探讨了自动生成命题逻辑系统R的可读证明。采用试探法和自然推理法分别从前推和后推模拟人类思维求证,试探法根据推理规则将待证公式反向分解,自然推理法从假设出发根据推理规则生成新的公式。两种方法都实现了相干命题逻辑系统R的可读证明,并结合实现了混合证明。试探法和自然推理法是生成可读证明的有效方法,前推和后推两种思维方法也适用于其他逻辑系统的自动证明。

This paper discussed automatedly generating readable proofs for relevance propositional logic system R. This paper adopted probe method and natural deduction method, which simulated human mind forward and backward respectively, probe method backward decomposed formulas according deduction rules, and natural deduction method forward generated new formulas from hypothesis set according deduction rules. This paper abtained readable proofs for relevance propositional logic system R by two methods respectively and combining them. Probe method and natural deduction method are effective for generating readable proofs. Forward-deduction and backward-deduction are also suitable for automated reasoning in other logic systems.