摘要
在经典命题逻辑的学习中,公理系统L中的定理证明只能使用公理模式和推理规则,对于初学者而言,常常显得强人所难,主要表现为找不到证明的突破口.事实上,可以从两个方向出发:一方面,从公理模式出发,分析每条公理模式的特性,由此可得消件法和换位法两个小技巧;另一方面,通过使用演绎定理,一般我们可得到待证定理的演绎证明序列,而通过对演绎证明序列的“仔细观察”,可以获得相应公理证明的“突破口”.这些技巧,可以提高初学者的学习效率,优化数理逻辑的教学,也可以为定理机械化证明的理论和方法提供必要的实践准备,以促进新时代逻辑学教学现代化的实现.
基金项目
重庆市社会科学规划青年项目(2016QNZX04)
西南政法大学研究生科研创新项目(2017XZXS-032)
NETL
NSTL
万方数据