机器证明的困难所在

机器证明是人工智能的一个重要课题,即用计算机来证明定理,亦称自动证明或定理的机械化证明,其基础是由 Hibert 在1930年奠定的,60多年来历程艰苦,困难在于传统逻辑、三段论、充分条件、同理可证、直觉思维的局限性。如果我们正视这些困难,利用专家系统,机器学习等技术,机器证明将进入一个崭新的局面。