论文研究启发式方法生成命题逻辑可读证明.pdf

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