数理邏輯和自动化

建立以概念和命題为对象的字母演算的最早想法和尝試皆属于十七世紀著名的数学家和哲学家萊布尼茲(1646-1716)。根据这种邏輯演算的思想,他曾幻想有一天人們可以用計算去代替辯論。因而萊布尼茲设法使邏輯和計算結合起来,使邏輯代数化,把組合分析的思想灌輸到邏輯中去,即建立現在称为数理邏輯的这門科学。数理邏輯发展到今天已达高度完善的程度,并成为最主要的数学学科之一。数学基础和数理邏輯現在也几乎变为同义語了。今天任何一篇有关数学現状及其发展的途的較长的綜合性文章部首先要考察数学基础和数理邏輯。这很自然,因为一方面研究数理邏輯并不需要任何的数学預备知識,另方面数理邏輯对現代数学的所有各分支却是必不可少的,因为現代数理邏輯的研究对象是建立数学証明的方法和工具。現代的数理邏輯可定义为研究数学証明的科学。