duvAAA吴文俊与数学机械化

吴文俊与数学机械化 纪志刚 上海交通大学学报,2001 年第3 期 摘要:机器证明的思想可以回溯到17 世纪的Descartes 与Leibnize ,20 世纪初Hilbert 更明确地提出了公理系