数理逻辑的发展早期主要是研究数学基础问题。虽然这方面没有取得预想的成功，但是数理逻辑的研究揭示了：推理和计算都是从初始符号串出发执行几个简单规则或操作的过程。Church-Turing论题使得人们有理由认为各种过程（如思维过程、通讯、进程）都可看作是计算因而可以用逻辑的方法进行刻画。这就是所谓的形式化方法。形式化方法建立了软件工程的逻辑基础，成为软件设计和开发的严格方法及工具。形式化方法已被软件工业界所采用，特别是用于严格安全系统的研制。

我国数理逻辑的开拓者们也都注意到了数理逻辑和计算机科学及人工智能之间的天然联系。20世纪50年代胡世华倡导数理逻辑在计算机科学中的应用研究。在1960年代初，莫绍揆亲自参加过一些计算机的研究工作。在1980年代，莫绍揆还参加由计算机科学家徐家福、孙钟秀主持的“五代机”讨论班。吴允曾在1970年代由数理逻辑转到计算机理论研究，带领其团队开展“形式化方法”的研究sup[143]。

唐稚松在清华大学读大学时，就学习数理逻辑。早在1965年，唐稚松在《数学学报》发表了一篇关于计算机指令系统性质的论文，提出转移指令可用循环替代。这一结果比国外同行的类似结果早发表一年。20世纪70年代中期，唐稚松分析总结了国际上结构程序设计研究方面的大量资料，完成了长篇论文“结构程序设计与结构程序语言”。在此基础上，他设计了一个广谱的结构程序语言，取名为系列化语言族，简称XYZ系统。在1980年代，唐稚松为XYZ建立了时序逻辑基础，提出了可执行时序逻辑语言XYZ/E。该语言将状态转换的控制机制引入到逻辑系统之中，又将这种时序逻辑形式化理论与最新软件技术结合起来sup[23][107]。

周巢尘在研究生期间师从胡世华院士，研读数理逻辑。自1970年代中期，致力于程序验证和代数符号计算研究sup[171]。他以一阶谓词演算为工具研究程序模式，证明了程序模式的基本特性的不可判定性sup[172]。1980年代，周巢尘从事通信顺序进程的CSP的正确性证明，研究大规模分布式系统的内在结构，发展了组合验证技术sup[173]。之后，周致力于实时系统的模型、语义描述及其正确性的研究。提出了一阶谓词时序逻辑——时段逻辑。时段演算是用于嵌入式实时软件系统设计的演算系统。它是区间时态逻辑的扩展，可用于处理数学分析中函数在连续时间上的一些概念，如：积分、平均值、分段连续性和可微性。该演算能够应用于对混合系统的实时需求进行刻画和精化，同时也能定义计算系统的实时行为和语义sup[53]。

R.Milner在1970年代首先提出了描述通信系统并发行为的形式演算CCS。然而CCS的交错语义并非是真正的并发语义。为了给出CCS的真正意义上的并发语义，P.Degano，R.De Nicola和U.G.Montanari提出了contact-free A-C/E系统。然而这个系统是不完全的（比如，没有关于递归主体和非确定主体的并发）。陆汝钤把数学中黎曼曲面的思想引进PETRI网论，建立了多层PETRI网模型Petri/Riemann（P/R）网，以定义A-C/E系统。陆应用P/R网给出了CCS的完全真并发语义，解决了其特有的（在双模拟意义下的）语义等价问题sup[299]。陆汝钤把原来只能描述静态控制结构的代数语义推广到能描述动态控制结构，使代数语义具备了描述完整程序控制结构的能力，从而真正体现了“对代数语义来说，程序即抽象数据类型”这一论题sup[306][307]。

林惠民长期从事计算机程序，特别是并发程序的形式语义学及形式化方法的研究。他提炼出了一个元语言，用它可以描述各种进程演算的公理化语义，并且具有良好的可读性。在此基础上实现了通用的交互式进程代数验证工具PAMsup[242][243]。林惠民与英国Sussex大学的Hennessy教授合作，提出了“符号互模拟理论”。他们引入了“符号迁移图”，在此基础上建立了符号互模拟理论，进一步建立了消息传送进程互模拟的相对完备证明系统sup[310][311]。为了描述移动式通信，ACM图林奖获得者Milner教授与其合作者于1989年正式提出π-演算（也称“移动进程演算”）。π演算研究中的一个基本问题是刻画进程的互模拟等价关系。为了对π-演算中递归定义的无穷进程进行推理，林针对π-演算建立了符号互模拟的理论。林惠民在1995年发表了π-演算迟、早两种弱互模拟的完备证明系统sup[240]。为了对π-演算中递归定义的无穷进程进行推理，林在π-演算中引入“进程抽象”的构造，并进一步发展了有穷控制π-演算弱互模拟的完备证明系统sup[241]。

计算模型是逻辑学和计算机科学研究的重要问题。λ-演算是顺序计算的理论模型之一。为了找到一个可与λ-演算相比的并发计算模型，Milner等人提出了π-演算。借鉴证明论中的一些思想，傅育熙提出了并发计算的一个图模型。在此模型中，计算对象表示为图，计算过程表示为图重写，重写规则将通信过程视为证明的等价变换过程。为便于形式化研究图模型，提出了模型的形式对应物——图演算sup[24]。在并发计算图模型的基础上，傅育熙提出一种新型并发计算模型——χ-演算。该演算的创新处在于它只有一类前缀操作，故通信是对称的。χ-演算与π-演算的不同之处在于：具有统一的输入和输出，只有一类受限名，通信的范围由局部化操作子界定，允许更大的并发度sup[25][233]。χ-演算的引入有两方面的考虑：（1）纠正χ-演算中前缀操作子的不规范性，统一进程代数中的各类名；（2）将证明论中的一些思想引入并行理论。π-与χ-的主要区别在于通信机制，前者采用值传送的通信方法，后者采用信息交换的通信方法sup[28]。傅育熙还给出π-演算到χ-演算的转换，从而，前者是后者的子语言。傅育熙还给出了一个高阶χ-演算sup[234]。在有关χ-演算的基础上，傅育熙用统一的方法在χ-进程上引入一大类互模拟等价关系，即L-互模拟等价关系。证明了只有4个不同的L-互模拟等价；在包含关系下，它们构成钻石格。许多常见的互模拟等价都可定义为L-互模拟等价sup[26]。在χ-进程间互模拟格的基础上，利用L-互模拟的开刻画，给出所有4个L-互模拟等价诱导的同余关系的完全公理化系统IVsup[27]。

前面提到的π-演算预设了通信频道是无噪声的，但在实际的移动系统中这是不可能的。为此，应明生提出了πN演算，它允许噪音出现。应明生提出了该演算中的近似强互模拟和等价关系，建立了各种代数定律。他还引进了可靠性已比较各主体的行为。应明生的工作为处理移动系统的可靠性和正确性提供了工具和技术sup[369][370]。

胡国定在1988年引进了可计算模型的构造型定义，记作MMCM。这是一个一般的定义，已有的计算模型如图灵机、Post系统等，以及一阶逻辑系统，公理集合论系统都是特殊的MMCM系统sup[253]。

孙永强早在1980年代探讨如何以模态逻辑为形式化工具对顺序、并发以及非确定性程序的论证sup[104][179]。1995年以来，何积丰与C.A.R.Hoare提出了程序设计统一理论和连接各类程序理论的数学法则。还提出了用形式化的界面理论沟通几种程序语言sup[55][246]。

自动机是对信号序列进行逻辑处理的装置，可定义为一种逻辑结构，一种算法或一种符号串变换。在计算机科学中自动机用作计算机和计算过程的动态数学模型，用来研究计算机的体系结构、逻辑操作、程序设计乃至计算复杂性理论。在语言学中则把自动机作为语言识别器，用来研究各种形式语言。在神经生理学中把自动机定义为神经网络的动态模型，用来研究神经生理活动和思维规律，探索人脑的机制。在生物学中有人把自动机作为生命体的生长发育模型，研究新陈代谢和遗传变异。在数学中则用自动机定义可计算函数，研究各种算法。现代自动机的一个重要特点是能与外界交换信息，并根据交换得来的信息改变自己的动作，即改变自己的功能，甚至改变自己的结构，以适应外界的变化。也就是说在一定程度上具有类似于生命有机体那样的适应环境变化的能力。

马希文早在1978年引进树计算机和这种计算机上的程序——树程序的概念，并进行了有关的讨论。他希望说明，在研究形式语言和编译系统的某些问题时，树计算机和树程序可能成为一种有效的工具sup[68]。

关于线性自动机的理论，早在20世纪60年代初，汪湘浩引进了圈环的概念，以此为出发点，管纪文在线性自动机的分析和综合问题上取得了一系列成果sup[30]。

陶仁骥大学毕业后也曾在中国科学院数理逻辑室工作。陶后来在自动机理论中独创了“可逆有限自动机理论”，并在该理论的基础上，提出和发展了“有限自动机公开钥”方法sup[108][342]。

洪加威除了在计算复杂性方面的成果外，还研究形式文法sup[31][32]。董韫美研究形式规约的获取与复用，提出基于复用的文法推断方法，并提出一种新的递归函数理论：上下文无关语言上的递归函数CFRFsup[20][21]。

陆汝钤和郑宏提出了格值有穷状态量子自动机（LQA）的量子计算理论。他们引进了推广的pumping性质，并证明对于LQA，推广的pumping引理成立sup[302][303]。邱道文与应明生引进了一种新的量子有穷自动机（qGFA）和相应的量子正规文法（qQRGs），证明了两者不仅等价，还与MOQFA（仅测一次量子有穷自动机）等价sup[322]。

量子逻辑早在1936年就被G.Birkhoff和J.von Neumann提出，量子计算近年来也有了长足的发展。应明生建立了基于量子逻辑的计算理论。他首先定义了正交模格值量子自动机，在量子逻辑的框架内研究了这种自动机的性质。而后定义了被这种自动机所接受的正规语言（称作正交模格值正规语言），导出了这种语言的闭包性质。进而，把Kleene定理推广到了量子逻辑中。应明生证明了，基于量子逻辑的计算理论中的许多性质依赖于该逻辑的分配性质。从而揭示了，基于量子逻辑的计算理论与经典计算理论的本质差异。他还建立了基于量子逻辑的自动机理论的泵作用（pumping）引理sup[367][368]。

1968年由生物学家A.Lindenmayer提出的L系统是为把形式语言理论应用到发育生物学中而创立的一种并行重写系统，是描述生物体生长发育过程的数学理论，又叫Lindenmayer系统。但是，L系统及其种种变形刻画的都是同步的并发系统。实际上，在自然界中存在着许多异步的并发现象。因此，陆汝钤和张文妍对传统的L系统作了推广，提出了广义L系统的概念，证明了广义L系统不能被传统的L系统所覆盖，还划分了广义L系统的子类，证明了各子类等价的充分必要条件sup[61]。

刻画和描述认识过程中知识的进化和更新也是逻辑学方法的一个重要任务。而人类某个阶段在某一领域的知识可以看成是一个形式理论，李未把认知过程看成是形式理论的序列。他提出的开放逻辑就是关于形式理论序列的极限理论。开放逻辑中引进了猜想和反驳（事实反驳、归纳反驳）等基本概念；而后定义了形式系统在猜想或反驳下的重构；进而定义了形式理论序列的极限概念。李未还证明，开放逻辑可以刻画常识推理sup[282]。开放逻辑引起了国内外学者的关注，国内学者多关注极限存在性及重构算法的研究。开放逻辑的一个重要应用就是关于软件进化过程。我们知道，软件（如操作系统）都是在不断的完善和进化的。我们把某软件的一版本的规范（sepecification）看成是一个形式理论。因而软件的进化过程就是一个形式理论的序列。我们可以把新规则和用户意见看成是猜想与反驳，因而软件升级实际上就是形式理论在猜想或反驳下的重构sup[281]。

互联网是由分散的、在全球范围内相互链接的web文档构成的网络。20世纪末，Tim Berners Lee等提出语义web的设想，希望通过在web文档上附加机器能理解的语义标注，将互联网从文档web扩展成为数据web（数据库），从而可以以机器能理解的方式发布知识，进而实现知识集成和知识推理的自动化。在语义web中，所有信息都是具有语义的，语义表达是语义web最基本的问题。语义web的语义表达的主要问题就是应用领域的语义建模（包括建模语言的选择/设计）的问题。语义表达问题实际上可归结为本体理论在语义web中的应用问题。语义web中（本体的信息技术应用领域中）普遍接受的本体定义为：“本体是对某一个领域概念化的显式、形式化的描述”。我国学者在语义web的逻辑基础方面也作了重要工作。林作铨、刘升平等提出了语义定义语言XSDL、CKML、DAML+OIL和已成为W3C标准OWLsup[59]。DAML+OIL语言与描述逻辑SHOIQ（D）等价，OWL DL与描述逻辑SHOIN+（D）等价，SHOIQ（D）和SHOIN+（D）有可判定tableaux推理算法。由于对应关系的存在，这些语言的本体描述、推理问题的理论研究就可以归为对应描述逻辑的研究。描述逻辑不仅在语义web的理论研究中非常重要，在其具体应用中也非常重要，例如：在对本体推理时，DAML+OIL或OWL本体可以直接转换成对应描述逻辑的公式，之后推理问题的计算过程交给描述逻辑推理机完成就可以了。因此，描述逻辑的研究也受到了国内学者的重视（如见注释sup[45][46][71][97]）。韩婷婷等提出一种Tree-逻辑以刻画互联网中的半结构化数据sup[245]。

必须指出的是，逻辑方法还在机器学习、信息安全、计算语言学、认知科学、经济学等领域都有十分广泛的应用。例如，吕建和徐家福针对自学习软件自动化系统NDSAIL的需要，提出了保证归纳结论正确性的一致性准则和可满足性准则以及用多层次的演绎推理加以自动确认的方法，其主要特点是：（1）面向应用的归纳结论正确性准则；（2）验证功能与修正功能相结合的确认方法；（3）基于自动演绎机制的自动实现sup[65]。吕建等结合BDI结构和情境演算的优点，提出了一个能够刻画Agent的多种特征，尤其是自主性的智能体结构AASC（Agent architecture based on situation calculus）。此结构既能表示Agent的信念、目标、策略等心智状态，又能进行行动推理和规划，为解释Agent的自主性、建构不同类型的Agent提供了统一的平台sup[48]。为了将密码协议的非否认性和公平性统一在一个框架之下更好地进行分析，范钰丹和韩继红提出了一套适用于分析非否认性和公平性的一阶逻辑语法和语义。在此基础上建立了一个用于分析非否认性和公平性的一阶逻辑模型，证明了模型的有效性和正确性sup[22][70]。