计算机科学中的逻辑分类：①程序设计理论。霍尔（Hoare）逻辑（一种模态逻辑）、动态逻辑、命题-演算（一种高阶模态逻辑）。②数据库。阿姆斯特朗公理：关于函数依赖关系是可靠的并且完备的。③信息安全。BAN逻辑：一种多种多模态逻辑。④人工智能。BDI（belief-desire-intention）逻辑、动作逻辑、事件逻辑、情景演算等。

这些逻辑按照经典（亚里士多德考虑过的逻辑）和非经典分成如下两类：①经典逻辑。命题逻辑、谓词逻辑、模态逻辑。②非经典逻辑。时态逻辑、动态逻辑、非单调逻辑、描述逻辑等。

按照被形式化对象来分可以分为：①描述性质的逻辑。命题逻辑、谓词逻辑、模态逻辑、其中模态逻辑包括K,D,T,S4,S5系统。②描述对象的逻辑。描述逻辑、O-逻辑、F-逻辑、其中描述逻辑包括模态描述逻辑、时序描述逻辑、动态描述逻辑等。③描述元性质的逻辑。非单调逻辑、多值逻辑、模糊逻辑，其中非单调逻辑包括封闭世界假设、界定（circumscription）、自认知逻辑、缺省逻辑、非单调逻辑程序等。

多值逻辑包括3-值逻辑、线性值逻辑、布尔值逻辑、格值逻辑等。

德国数学家G.弗雷格（Gottlob Frege，1848-11-08～1925-07-26）给出了一个二阶谓词演算和概念理论，其中有一个概念的概括原理是说：每个公式定义一个概念，即：

式中为一个不含概念的公式。英国哲学家、数理逻辑学家B.A.W.罗素（Bertrand Arthur William Russell，1872-05-18～1970-02-02）发现了这个二阶谓词演算中蕴涵了著名的罗素悖论。德国数学家D.希尔伯特于20世纪20年代提出了希尔伯特计划，其目的是用并且只用严格的证明方法证明形式系统的协调性。1928年，D.希尔伯特与德国数学家W.阿克曼（Wilhelm Ackermann，1896-03-29～1962-12-24）写了第一本数理逻辑书（Grundzüge der theoretischen Logik），在该书中，他们提出了一个形式证明系统以及关于这个形式证明系统的2个问题：①该形式证明系统是否是完备的。②（算法问题）找一个算法来判定一个结论能否从一个或几个前提中通过形式推理的方法推出。

1930年，美籍奥地利数学家K.哥德尔证明了该形式证明系统是完备的，并于1934年证明了：在一个形式系统内证明该形式系统是否协调的是不可判定的。这里的不可判定性是指不能证明也不能否证。这是哥德尔不完全性定理的第二种形式。哥德尔不完全性定理是说：存在皮亚诺算术中的一个公式，使得在皮亚诺算术的标准模型中是真的，但是在皮亚诺算术中是不可证明的。由哥德尔完全性定理，在皮亚诺算术系统中也是不可证明的。哥德尔不完全性定理的证明使用了哥德尔编码，可计算函数的可表示性定理以及说谎者悖论。可计算函数的可表示性定理建立了逻辑与计算之间的关系。哥德尔不完全性定理说明了形式化方法的局限性。

算法问题中的算法存在预示着所有数学问题都存在算法解；如果存在一个问题没有算法解，那么算法问题也就没有算法解。英国计算机科学家A.M.图灵（Alan Mathison Turing，1912-06-23～1954-06-07）直观认为这样的算法不存在。对于存在算法的问题，找到直观的算法就可以。可以简单地判定一个算法是否是一个算法。因为直观算法定义为一个有限的、可以机械执行的指令集合。问题的困难之处在于：如果算法不存在而要证明它不存在。要证明该算法不存在，就需要严格定义的算法概念。1936年，A.M.图灵定义了图灵机以及通用图灵机，其中通用图灵机可以接受一个图灵机以及一个输入作为输入，通用图灵机将模拟所接受的图灵机在输入上的计算。这正是现代计算机的理论原型。图灵机的研究是数理逻辑分支之一：递归论，又称可计算性理论。

由于算法是一个直观的和非形式的定义的概念，而图灵机是严格的形式定义的概念。要证明所有图灵机可计算的自然数上函数等于所有算法可计算的函数，这是一件不可能证明的事情。因此，美国数学家A.丘奇（Alonzo Church，1903～1995）提出了丘奇-图灵假设（Church-Turing thesis）：所有算法可计算的函数是图灵可计算的。而算法在计算机科学中起着中心作用，见图。

算法在计算机科学中起着中心作用

一个计算模型是一类统一模式定义的计算设备，每个计算设备是由一个有限或者无限的符号集合，一个有限的状态集合，以及由符号和状态的序对到符号和状态的序对的有限函数组成，其中状态又分为一个开始状态，停机状态和中间状态。比如图灵机是一个计算模型，每个计算设备即是一个图灵机，符号集合是所有的0-1有限序列，一个有限的状态集合，以及有限函数是由一个{0,1}的符号和一个状态到一个{0,1}的符号和一个状态，以及一个左移或右移的序组组成；有限自动机是一个计算模型，每个计算设备是一个有限自动机，其中符号集合是一个有限字母表上有限序列组成的无穷集合、一个有限状态集合，以及有限函数是由一个字母和一个状态组成的序对到一个字母和一个状态组成的序对的有限映射。当设备的符号集合为自然数集合或者0-1的有限序列组成的无限集合，那么每个输入符号（开始状态的符号）对应一个输出符号（停机状态的符号），即该设备定义一个自然数上的一个函数。比如图灵机的有限{0,1}-序列是自然数的编码，输出也是一个有限{0,1}-序列，那么输入到输出的函数是一个自然数上的函数，称为图灵可计算函数；如果一个自然数上的函数不存在一个图灵机来计算该函数，则该函数称为图灵不可计算函数。同样也可以定义自然数的有限状态自动机可计算的函数和有限状态自动机不可计算的函数。

计算模型有10多种，包括递归函数、-演算、有限自动机、形式语言、重写系统等。提出这些计算模型的目的是严格定义算法这个直观概念。图灵证明算法问题是图灵不可解的。很容易判断：图灵可计算函数是算法可计算的，并且每个计算模型上可计算的函数都是算法可计算的。这里机械性反映在指令集合的有限性上，在每个符号和指令的情况下，至多只有有限多个可能的符号和指令的序对是该符号和指令的下一个构件（configuration）。

所有这些计算模型的计算能力是等价的，即所有计算模型计算的自然数函数类是相同的。给定两个计算模型和，如果存在一个映射将上的一个计算设备映射到上的一个计算设备，并且反过来，存在一个映射将上的一个计算设备映射到上的一个计算设备，并且和是互逆的，即，，那么计算模型和在计算能力上是等价的。此结论说明：人们找不到一个计算模型使得存在一个该模型上的计算设备计算出的函数在已有的计算模型中是不可计算的。由此导致了丘奇-图灵（Church-Turing）假设：每个算法可计算的函数是图灵可计算的。

此外，和的计算复杂性是相同的，并且和的计算复杂性也是相同的。也就是说：计算模型的选择不能改变一个计算问题的可计算性，同时也不能改变一个计算问题的计算复杂性。

在以图灵机为计算模型下，图灵机的转换关系是带概率的计算。

一个概率图灵机是一个六元组，其中分别为打印符号集合和辅助集合；为内部状态集合；为初始状态为的概率，为当前状态为并且输入为时下一个状态为和输入为的概率；并且为一个到[0,1]的函数，满足下列条件：对每个和，并且。

式中：

：用替换并且到状态；

：右移一格并且到状态；

：左移一格并且到状态；

：停止；

：根据一个随机集合，要么到要么到状态。

因而，一个概率图灵机是一个非确定图灵机，其转换关系是根据概率分布来决定的。

E.S.桑托斯（Eugene S.Santos）于1971年提出概率图灵机以及基于其的可计算理论。类似地可以定义相对概率图灵机以及概率部分可计算的随机函数。部分可计算的普通函数（非随机的函数）类证明等于部分递归函数类。并且存在一个概率部分可计算的普通函数类真包含部分递归函数类。在某种意义下，概率图灵机可以计算自然数上的任何函数。

另一种定义为：一个概率图灵机是一个图灵机，其转换关系为2个，其中在输入为的情况下，人们每步以1/2的概率选择转换关系，并且以1/2的概率选择转换关系。