[敬请读者注意] 本人保留本文的全部著作权利。如果哪位读者使用本文所描述内容，请务必如实引用并明白注明本文出处。如果本人发现任何人擅自使用本文任何部分内容而不明白注明出处，恕本人在网上广泛公布侵权者姓名。敬请各位读者注意，谢谢！

强相关逻辑及其应用（下）

程京德 

[注：本文为笔者2016年发表在科技导报第34卷第7号上的文章“相关推论与强相关逻辑”（迄今为止唯一的一篇关于强相关逻辑的中文文献）之修改增补版，更换标题为“强相关逻辑及其应用”，发表在此。]    

    概要：推理的能力，尤其是抽象推理的能力，无疑是人类智能最本质的特征之一，因而应该是任何以实现人工通用智能为目标的人工智能系统都应该提供的必不可少的最基本功能。本文介绍构建强相关逻辑的动机，展示强相关逻辑的各种应用，并且指出，为相关推理提供逻辑有效性保证的强相关逻辑，对于以推理、发现、预测为最基本功能的各种人工智能系统来说，具有无可替代的关键作用。强相关逻辑是实现人工通用智能不可或缺的逻辑基础。

基于强相关逻辑的相关推理在发现和预测中的关键作用

发现是寻找出或者揭示出某个前所未知（发现者本人前所未知或者全世界的人们都前所未知）的事物的过程。预测是预先猜测出在某个未来时刻（因此是一个必定伴随有某个时间参照点的概念）发生某个事件的过程。对于任何发现或者预测，其被发现的事物或者被预测的事件必然是在发现和预测完成之前预先未知的，否则，就完全没有必要去发现已知的事物或者预测已知的事件了。由于推理是从给定前提获得预先未知的新结论之唯一途径，因此，不存在有完全不祈求于推理的发现和预测。

因为对于任何发现或预测来说，在发现过程或预测过程之前都没有一个完全明确地定义清楚了的目标（注意，如果有了这样一个目标，那么那将是一个证明而不是一个推理），并且被发现的事物或被预测的事件以及它们的真实性在发现过程或预测过程完成之前都是未知的，所以要求在发现或预测时所进行的推理必须是相关的这一要求是必然合理的。这个要求，对于科学发现或预测来说，在哲学意义上是本质重要的；这是因为，为了评估被发现的事物或被预测的事件，科学家们必须遵循最一般的、独立于科学家们正在实践的内容的正确性标准，它可以给出被发现的事物或被预测的事件的健全性保证。那么，最一般的标准是什么？在哪里我们可以找到最一般的标准？正是逻辑学，作为“科学之科学，技艺之技艺”、“所有其它科学之基础”、“先于所有其它科学，以其思想和原理支撑所有科学之科学”，可以提供这样的标准；正是强相关逻辑，可以圆满地支持相关推理，使得科学家们能够以非循环的、非同义反复的方式来评估所发现的事物或所预测的事件。

基于强相关逻辑的相关推理在各个领域各种实践中的发现和预测中有着广泛的应用前景。如果某个应用需要寻找独立于具体领域的、一般的逻辑有效性标准，使得只要保证了前提的正确性之后，对依据该逻辑有效性标准推出的结论无需再评价就可以直接接受为正确的，那么目前世界上符合此要求的只有强相关逻辑而无其它。

在充分条件关系意义下的强相关性对于任何发现和预测中的有效推理来说都是必不可少的；如果我们真的希冀要通过推理来发现新的事物或预测未来事件，那么我们应该求助于相关推理；事实上，当我们发现了一些新的事物或者预测了一些未来事件的时候，我们正是有意识地或无意识地进行了相关推理。

形式理论：将形式逻辑系统应用于具体对象领域的逻辑基础

一个形式逻辑系统是一个形式演绎系统，由其形式语言（由该逻辑系统的符号表中的符号构成的合乎文法的逻辑式的集合，用来表达逻辑命题）和逻辑归结关系（定义在该逻辑系统的语言上的、从语言的幂集到语言的二元关系，用来表达从前提推出有效结论）这两个部分构成。在一个形式逻辑系统中，所有无需前提就被认可为有效结论的逻辑式（亦即，逻辑归结关系中第一个元素为空集的有序对的第二个元素），被称为该逻辑系统的逻辑定理。依据对逻辑归结关系的不同表达方式，一个形式逻辑系统可以被表达为不同形式的演绎系统，比如，希尔伯特式形式化公理系统(Hilbert Style Formal Logic Systems)、根岑式自然演绎系统(Gentzen’s Natural Deduction System)、根岑式矢列演算系统(Gentzen’s Sequent Calculus System) 、语义表系统(Semantic Tableau System) 、解消原理系统(Resolution System)等等。但是，无论一个形式逻辑系统怎么被表达，其逻辑定理集合是一定不变的。

一个形式逻辑系统提供了对于论证和推理之逻辑有效性进行判断的某种形式化的一般逻辑标准。这个标准可以被用来判断，从给定的前提（由该形式逻辑系统的形式语言表达的逻辑式集合）能够得出什么样的逻辑上有效的结论（由该形式逻辑系统的形式语言表达的逻辑式）。不同的形式逻辑系统当然就提供了不同的逻辑标准，在某个形式逻辑系统下可以被判断为逻辑上有效的论证和推理，在另外一个形式逻辑系统下就可能被判断为逻辑上不有效的。所以，当我们要应用形式逻辑系统来解决具体对象领域内的问题的时候，首要的事情就是要根据目的来选择一个适当的形式逻辑系统。

从逻辑学的角度来说，逻辑学不关心各个具体对象领域内每个命题自身的真假对错，只关心从什么样的前提能够得出什么样的逻辑上有效的结论。

一个关于某个具体对象领域的形式理论是建立在选定一个形式逻辑系统作为其逻辑基础之上的形式演绎系统。当我们选定某个形式逻辑系统作为逻辑基础，并且确定了具体对象领域内被我们认定为真的经验公理之后，我们就在理论上确定了一个关于该具体对象领域的形式理论。

一个形式理论由两部分构成，其一为其基础逻辑系统的全部逻辑定理，其二为以经验公理为前提基于基础逻辑系统可以逻辑上有效地推出的所有经验定理。如下图所示：设所选定形式逻辑系统L的形式语言为F(L)，F(L)中所有的逻辑式被以P为前提基于L的形式理论划分为三部分，逻辑理论部分（L的全部逻辑定理，图中用红色表示）、经验理论部分（以经验公理集合P为前提基于L可以逻辑上有效地推出的所有经验定理，图中用蓝色表示）、非理论部分（F(L)中所有不被该形式理论所承认的逻辑式，图中用白色表示）。

比如，NBG(Neumann-Bernays-Gödel)公理集合论或者ZF(Zermelo-Fraenkel)公理集合论，就都是基于经典数理逻辑一阶谓词演算的、具有等词（将相等定义为一个初始谓词）的形式理论。两者的逻辑理论部分都是具有等词的经典一阶谓词演算，经验公理集合分别为NBG公理或者ZF公理。

从应用的观点来看，对于一个形式理论，我们一般关心，我们能够发现什么经验定理，或者我们能够证明什么经验定理，如下图所示。

从理论的观点来看，对于一个形式理论，我们一般关心它有何整体上的性质，亦即，关于该形式理论自身的元定理，如下图所示。

强相关逻辑作为各种应用逻辑的核心 

人类社会现代文明的发展对于古老的逻辑学提出了许多新的要求，尽管在亚里士多德的著作中已经有了模态概念，但是现今的各种哲学逻辑是起源于现代模态逻辑的研究[3,6]。

现在，逻辑学界通常把各种逻辑学划归为两大门类，经典数理逻辑（经典逻辑演算、公理集合论、递归函数论、模型论、证明论）[22] 以及哲学逻辑（所有的非经典逻辑），而几乎所有的哲学逻辑都是经典逻辑演算的某种保存扩张 [23-27]。许多基于经典逻辑演算的哲学逻辑系统通常都是针对经典逻辑演算的目标语言引入模态算子并且按照其哲学观点对模态算子的解释来引入相应的逻辑公理。这些哲学逻辑系统在被应用于各个应用领域内的证明/验证时，和经典数理逻辑被应用到数学领域内的证明/验证时一样，不会有什么问题。但是，如果把它们应用于推理、发现、预测的时候，就会遭遇到和经典数理逻辑被应用到推理、发现、预测的时候同样的各种问题。

笔者以强相关逻辑为核心，构建了各种基于强相关逻辑的哲学逻辑系统，包括时态相关逻辑(Temporal Relevant Logic)[28-33]，空间相关逻辑(Spatial Relevant Logic)[34]，时空相关逻辑(Spatio-temporal Relevant Logic)[35-38]，规范相关逻辑(Deontic Relevant Logic)[39-41]，时态规范相关逻辑(Temporal Deontic Relevant Logic)[42]等。将这些基于强相关逻辑的哲学逻辑系统应用于各个应用领域内的推理、发现、预测的时候，就不会出现基于经典数理逻辑的哲学逻辑系统被应用到推理、发现、预测的时候出现的各种问题 [43]。

另一方面，以 Garrett Birkhoff 及 John von Neumann 提出的量子逻辑为首的各种现代量子逻辑系统，也都存在有蕴涵悖论等问题。从哲学逻辑的观点来看，构建量子相关逻辑或者相关量子逻辑（两者区别在于以哪种逻辑作为基础逻辑来进行改良及扩张）的工作，是值得做的；从实现通用量子计算的观点来看，也可能是必须要做的 [44]。 

通用归结演算自动前推引擎EnCal及FreeEnCal 

因为在强相关逻辑的各种实践应用中，前推的自动化都是一个关键，我们先来介绍一下由笔者及学生们设计开发的通用归结演算自动前推引擎EnCal 及 FreeEnCal [45,46]。

因为强相关逻辑可以作为基础逻辑系统来支撑相关推理，所以，基于强相关逻辑的前推(forward reasoning)自动化就有了十分重要的实践应用意义。

简单粗略地说，EnCal (An Automated Forward Deduction System for General-Purpose Entailment Calculus) 就是一个实现前推规则分离规则(Modus Ponens)自动化的前推引擎，它以一个形式逻辑系统的逻辑公理模式作为输入，可以自动生成相应的逻辑定理模式作为该逻辑系统的断片；它以由它生成的形式逻辑系统断片以及某个领域的经验公理集合P作为输入，可以自动生成基于该形式逻辑系统的以P为前提的形式理论的经验定理。

FreeEnCal 是 EnCal 的更加通用版本。 EnCal 仅仅实现了前推规则分离规则的自动化，如果为了从逻辑公理模式高效地生成逻辑定理模式而应用其它推理规则，那么就需要对 EnCal 重新编程，加入新的程序模块来实现其它推理规则的自动化。与 EnCal 相比，FreeEnCal 的功能更强在于两点：(1) 它具备了根据输入的推理规则形式化描述自动地解释执行来实现推理规则自动化；(2) 它允许目标逻辑系统使用模态算子。

关于 EnCal 及 FreeEnCal 的实践应用还有一个很重要的技术问题。众所周知，一个形式化逻辑系统一般尽管仅有有限数量的公理模式，但是其逻辑定理模式却可以是无穷多（与自然数一样地可数个多）个。因此，自动生成一个实用的形式化逻辑系统的全部逻辑定理模式在实践上是不可能的，我们需要引入某种限制使得前推引擎自动生成的逻辑定理模式数量被合理地控制在一个有限范围之内。笔者提出的限制方法是对逻辑联结词在逻辑式中的嵌套深度(degree)进行限制，其本质是强迫前推引擎的使用者（或者在将来由前推引擎自身自动地）抽象出新概念(谓词)来表达复杂的逻辑式。所以，EnCal 及 FreeEnCal 的输入数据当中还有对各个逻辑联结词（最重要的当然是对初始内涵连接词必然归结(entailment)）的允许嵌套深度。

基于强相关逻辑的自动定理发现 

美国数学家、自动推理领域专家Larry Wos 在1988年提出了33个自动推理领域的未解决重要问题，其中第31个问题就是自动定理发现(Automated Theorem Finding, ATF)问题：“What properties can be identified to permit an automated reasoning program to find new and interesting theorems, as opposed to proving conjectured theorems?” [47,48]。

ATF问题被提出30多年来，至今仍未完全解决。ATF问题有几个基本要求：（1）要求“发现”而不是“证明”定理，（2）要求发现“新”并且“有趣”的定理（因此，形式地定义清楚“新”和“有趣”就是必要的），（3）要求识别出那些“特性”使得能够让自动推理程序发现定理。正是这几个要求中包含的一般性，使得该问题成为一个难题；然而也正是因为这些一般性，使得该问题之解决意义重大，应用广泛。

笔者在1994年就提出，从问题所要求的一般性来说，解决ATF问题必须依赖于合适的形式逻辑系统，经典数理逻辑不可能被用做解决ATF问题的基础逻辑，唯一有希望的候补逻辑系统应该是强相关逻辑 [9.10]。

下面介绍笔者和学生们利用FreeEnCal来解决ATF问题的尝试 [49-61]。

首先，我们选定谓词强相关逻辑系统EcQ作为解决ATF问题的基础逻辑系统，限定3(3rd degree)为初始内涵连接词必然归结的最高度，适当地限定联言连接词和否定连接词的度，用FreeEnCal来生成EcQ的逻辑定理断片。

其次，我们选择了NBG公理集合论，Peano算术，Tarski几何，图论作为基于EcQ之形式理论的对象领域，用FreeEnCal来生成各个领域的经验定理。由于笔者研究室计算机资源和算力的条件限制，我们只是“再发现”了一些简单的经验定理，在原理上验证了方法论的可行性。尽管我们仅选取了离散数学的几个领域来做实验，但是，从原理上来说，我们的方法论应用到任何其它专业对象领域去是毫无问题的，只要对象领域的公理化问题可以适当地解决。笔者相信，如果有更丰富的计算机资源和算力可以利用，在基于强相关逻辑的前推来实现自动定理发现这个方向上，将一定能够做出具有实践应用意义的结果。

另外，我们针对进行实验的几个领域，也做了自动抽象概念以及建立经验定理“有趣性”评价标准和尺度的尝试性工作。

请注意，尽管自动定理发现问题原本是从发现数学定理的角度提出的，但是，只要我们能够将某个具体领域的知识形式化地表达为一个形式理论，那么该领域内的推理、发现、预测问题就都可以转化为在该形式理论中的经验定理发现问题。因此，可以说，自动定理发现为几乎所有以前推作为解决问题必要手段的应用都提供了方法论基础。

基于强相关逻辑的认知过程模型以及认知程序设计系统

科学发现认知过程的模型化形式化，与科学发现的逻辑一样，一直都是科学哲学中的重要课题[13,14]。虽然试图阐明科学发现的一般机制在历史上从来都是科学哲学家和逻辑学家的研究课题之一，但是在计算机科学和人工智能领域，只有极少数学者在做试图把科学发现过程算法化自动化的研究工作（图灵奖和诺贝尔奖获得者 Herbert A. Simon 和他的部分学生是先驱）。

自1994年起，笔者试图基于强相关逻辑来对科学发现认知过程(epistemic processes in scientific discovery)模型化形式化，试图为科学家们提供描述科学发现认知过程的形式化手段（认知程序设计语言），并且将科学家们描述的科学发现认知过程实现自动化或半自动化（认知程序运行系统）[11,33,62-70]。实际上，强相关逻辑系统的构建正是在对科学发现认知过程模型化形式化的过程中最终完成的 [11]。

笔者在1998-2000年间提出了科学发现认知过程的强相关逻辑模型 [11]，提出了“认知程序设计(Epistemic Programming)”这一新的程序设计范式 [62-67]，并且与学生们一起设计和实现了认知程序设计语言EPLAS(Epistemic Programming Language for All Scientists) [68-70]。认知程序设计与传统的命令式程序设计不同之处在于：传统的命令式程序设计以变量的值作为计算对象，以对变量（计算机内的存储单元）的破坏性赋值作为改变计算状态的唯一操作手段，以算法控制结构作为程序设计的对象；而认知程序设计以条件句（条件关系）作为计算对象，以基本认知操作作为改变认知状态的操作手段，以认知过程作为程序设计的对象。认知程序设计范式试图为科学家们提供编制认知程序来让自己在科学发现过程中的认知过程实现自动化或半自动化的手段。

强相关逻辑的其它应用 

知识处理系统的自律进化：让知识处理系统具备自律进化的能力，从来都是人工智能领域的挑战性课题。笔者提出的研究方向是知识处理系统推理规则的自动生成和自动评价。笔者认为，只有在元层次（亦即，以知识处理操作作为处理对象的层次，可以一层一层地分层抽象化下去）上进行的形式化逻辑演算，尤其是基于强相关逻辑的自动前推，才能在机制上解决自律进化问题[71,72]。

超前预测反应系统：“超前系统(Anticipatory System)”是由加拿大数学家 Robert Rosen 于1985年提出的: “an anticipatory system is one in which present change of state depends upon future circumstance, rather than merely on the present or past.” Rosen 将超前系统定义为：“a system containing a predictive model of itself and/or its environment, which allows it to change state at an instant in accord with the model’s prediction to a latter instant.”[73] 比利时系统科学家 Daniel M. Dubois 从计算系统的观点定义了“计算超前系统(Computing Anticipatory System)”[74]。传统的反应系统(Reactive System)仅仅具备被动反应能力而不足以主动对应即将发生的可靠性安全性问题，笔者从改善并提高传统反应系统之能力的角度出发，提出了基于时态相关逻辑的超前预测反应系统(Anticipatory Reasoning-Reacting System)作为传统反应系统的扩张，并且与学生们一起开展了超前预测反应系统在航管调度、高层电梯救生、机场地面调度等方面的应用尝试 [30,75-81]。

基于规范相关逻辑的法律知识表达与推理：在任何一个基于法制的法治社会，法律法规中隐含有矛盾、法庭辩论中隐含有矛盾、审判依据中隐含有矛盾等情形，都会给社会给当事人造成不好的影响，解决这一问题的正确方向显然应该是法律法规的完全形式化验证以及基于準一致逻辑(paraconsistent logic)系统的準一致推理(paraconsistent reasoning)。但是，由于经典数理逻辑及其各种经典保存扩张或者非经典替代中都包含有蕴含悖论ECQ(从矛盾可以推出一切)，形式化逻辑系统从来就没有在法律学领域及公检法实践中发挥出所被期待的作用。对此，笔者提出的研究方向是以具有準一致性的规范相关逻辑作为法律知识表达与推理的逻辑基础，以基于规范相关逻辑的準一致相关推理作为在可能有隐含矛盾的景情下的推理手段 [39-41]。

密码协议推理：因为信息安全性工程是要保障不让不应允许的、破坏信息安全性（有时也包括公平性）的攻击或破坏行为造成破坏，亦即，保证某种“不可能”，所以是一件很难的事情。现实社会中常常出现已经应用到实际系统的密码协议对新的攻击方法有漏洞而必须重新设计的情形。因此，如果能够从已知的知识和假设而推理出未知的漏洞或者可能的攻击方法，则将是非常有用的。笔者提出的研究方向是以基于规范相关逻辑的相关推理来发现未知的漏洞和预测可能的攻击方法[82-90]。

动态意图计算：人们的意图，往往会依据现实环境中周围情况的变化而变化，在许多实际应用中，准确地及时地把握用户在付诸行动之前的最终意图十分重要，但是这却不是能够轻易并及时得到的。笔者提出了以三元时空相关逻辑为基础的“动态意图计算”研究方向，试图让意图计算可以应用高速计算机来进行，以相关逻辑来保证预测的准确性，以高速计算来保证预测的及时性 [20]。

自动知识增值：笔者提出了自动知识增值(Automated Knowledge Appreciation)这一研究方向,试图基于强相关逻辑建立知识价值演算体系作为可动态调节的价值判断标准，与自动定理发现系统一道，用来为计算系统智能化提供一般的自动化手段 [21]。

结语 

从逻辑学理论来说，强相关逻辑，作为目前最为严谨合理地定义了条件句概念/充分条件关系的逻辑系统，在为推理、发现、预测提供最一般的逻辑标准方面，有着其它逻辑系统无可替代的地位，能够作为其它应用逻辑系统的核心基础。

从智能科学和知识科学来说，如果需要构筑并且的确能够构筑一个统一的理论基础，那么，这个统一的理论基础必然基于强相关逻辑。

从人工智能技术来说，为相关推理提供逻辑有效性保证的强相关逻辑，对于以推理、发现、预测为最基本功能的各种人工智能系统来说，具有无可替代的关键作用。强相关逻辑是实现人工通用智能不可或缺的逻辑基础。

参考文献

[1] 程京德, “逻辑学是什么？” 微信公众号“数理逻辑与哲学逻辑”，2023年1月25日。

[2] R. Anderson, and N. D. Belnap Jr., “Entailment: The Logic of Relevance and Necessity, Vol. I,” Princeton University Press, Princeton, 1975. 

[3] W. Kneale and M. Kneale, “The Development of Logic,” Oxford Clarendon Press, 1962, 1984 (Paperback Edition with Corrections); 中译：张家龙，洪汉鼎 译 “逻辑学的发展”，商务印书馆, 1985.  

[4] 王宪钧, “数理逻辑引论”，北京大学出版社，1982, 1998. 

[5] S. Read, “Relevant Logic: A Philosophical Examination of Inference,” Basil Blackwell, Oxford, 1988, 2012. 

[6] L. Haaparanta (Ed.), “The Development of Modern Logic,” Oxford University Press, 2009. 

[7] W. Ackermann, “Begrundung Einer Strengen Implikation,” The Journal of Symbolic Logic, Vol. 21, pp. 113-128, 1956 (in German). 

[8] J. Cheng, “Rc - A Relevant Logic for Conditional Relation Representation and Reasoning,” Proceedings of the 1st Singapore International Conference on Intelligent Systems, pp. 171-176, Singapore, September 1992. 

[9] J. Cheng, “A Relevant Logic Approach to Automated Theorem Finding,” Proceedings of the Workshop on Automated Theorem Proving attached to International Symposium on Fifth Generation Computer Systems 1994, pp. 8-15, Tokyo, Japan, December 1994. 

[10] J. Cheng, “Entailment Calculus as the Logical Basis of Automated Theorem Finding in Scientific Discovery,” in “Systematic Methods of Scientific Discovery: Papers from the 1995 Spring Symposium,” AAAI Technical Report SS-95-03, pp. 105-110, AAAI Press, March 1995.

[11] J. Cheng, “A Strong Relevant Logic Model of Epistemic Processes in Scientific Discovery,” in E. Kawaguchi, H. Kangassalo, H. Jaakkola, and I. A. Hamid (Eds.), “Information Modeling and Knowledge Bases XI,” Frontiers in Artificial Intelligence and Applications, Vol. 61, pp. 136-159, IOS Press, February 2000. 

[12] M. R. Diaz, “Topics in the Logic of Relevance,” Philosophia Verlag, München, 1981. 

[13] M. V. Curd, “The Logic of Discovery: An Analysis of Three Approaches,” in T. Nickles (ed.), “Scientific Discovery, Logic, and Rationality,” pp. 201-219, D. Reidel, 1980. 

[14] T. Nickles, “Introductory Essay: Scientific Discovery and the Future of Philosophy of Science,” in T. Nickles (ed.), “Scientific Discovery, Logic, and Rationality,” pp. 1-59, D. Reidel, 1980. 

[15] E. D. Mares, “Relevant Logic: A Philosophical Interpretation,” Cambridge University Press, Cambridge, 2004. 

[16] J. Cheng, “Relevant Reasoning as the Logical Basis of Knowledge Engineering,” in F. J. Cantu, R. Soto, J. Liebowitz, and E. Sucar (Eds.), “Application of Advanced Information Technologies: 4th World Congress on Expert Systems, Mexico City, Mexico, March 1998,” Vol. 1, pp. 449-457, March 1998.

[17] J. Cheng, “Fuzziness and Relevance: Can We Establish a Unified Logical Basis for Approximate and Relevant Reasoning?” Proceedings of the 4th Asian Fuzzy Systems Symposium, pp. 875-880, Tsukuba, Japan, June 2000.

[18] J. Cheng, “Automated Knowledge Acquisition by Relevant Reasoning Based on Strong Relevant Logic,” in V. Palade, R. J. Howlett, and L. C. Jain (Eds.), “Knowledge-Based Intelligent Information and Engineering Systems, 7th International Conference, KES 2003, Oxford, UK, September 3-5, 2003, Proceedings, Part I,” Lecture Notes in Artificial Intelligence, Vol. 2773, pp. 68-80, Springer, September 2003.

[19] J. Cheng, “Relevant Reasoning: Its Key Role in Discovery and Prediction,” in Yaoxue ZHANG, Jingde CHENG, Jianhua MA, and Zhiliang ZHU (Eds.), “Forum of Future Computing: Discussion and Prospect, International Top-level Forum on Engineering Science and Technology Development Strategy, Chinese Academy of Engineering,” pp. 197-204, Northeastern University Press, August 2013.

[20] J. Cheng, “Computing Intentions Dynamically in a Changing World by Anticipatory Relevant Reasoning,” in N. T. Nguyen, B. Attachoo, B. Trawinski, and K. Somboonviwat (Eds.), “Intelligent Information and Database Systems, 6th Asian Conference, ACIIDS 2014, Bangkok, Thailand, April 7-9, 2014, Proceedings, Part II,” Lecture Notes in Artificial Intelligence, Vol. 8398, pp. 361-371, Springer, April 2014.

[21] J. Cheng, “Automated Knowledge Appreciation: A Relevant Reasoning Approach to Expand Our Knowledge and Increase Its Value Automatically,” Proceedings of the 14th IEEE International Conference on Cognitive Informatics & Cognitive Computing, pp. 175-183, Beijing, China, IEEE Computer Society Press, July 2015. 

[22] J. Barwise, “Handbook of Mathematical Logic,”Elsevier, 1977. 

[23] L. Goble (Ed.), “The Blackwell Guide to Philosophical Logic,” Blackwell, 2001. 

[24] D. Jacquette (Ed.),“Blackwell Companions to Philosophy - A Companion to Philosophical Logic,” Blackwell, 2002. 

[25] D. Jacquette (Ed.),“Philosophy of Logic – An Anthology,” Handbook of the Philosophy of Science, Elsevier, 2007. 

[26] D. M. Gabbay and F. Guenthner (Eds), “Handbook of Philosophical Logic, 2nd Edition,” Vol.1-18, Springer, 2001-2018. 

[27] G. Priest, “An Introduction to Non-Classical Logic, 2nd Edition,” Cambridge University Press, 2008.  

[28] J. Cheng, “Temporal Relevant Logic: What Is It and Why Study It?” Volume of Abstracts of the 11th IUHPS/DLMPS International Congress of Logic, Methodology and Philosophy of Science, p. 253, Cracow, Poland, International Union of History and Philosophy of Science, August 1999.

[29] J. Cheng, “Temporal Relevant Logic as the Logical Basis of Autonomous Evolutionary Information Systems,” Proceedings of the 2nd International Conference on Software Engineering, Artificial Intelligence, Networking & Parallel/Distributed Computing, pp. 770-777, Nagoya, Japan, ACIS, August 2001.

[30] J. Cheng, “Temporal Relevant Logic as the Logical Basis of Anticipatory Reasoning-Reacting Systems” (Invited Paper), in D. M. Dubois (Ed.), “Computing Anticipatory Systems: CASYS 2003 - Sixth International Conference, Liege, Belgium, 11-16 August 2003,” AIP Conference Proceedings, Vol. 718, pp. 362-375, American Institute of Physics, August 2004. (Best Paper Award awarded at the Sixth International Conference on Computing Anticipatory Systems). 

[31] J. Cheng, “Adaptive Prediction by Anticipatory Reasoning Based on Temporal Relevant Logic,” Proceedings of the 8th International Conference on Hybrid Intelligent Systems, pp. 410-416, Barcelona, Spain, IEEE Computer Society Press, September 2008.

[32] J. Cheng, “Temporal Relevant Logic in Adaptive Prediction,” in F. Wen, L. Yu, Y. Wang, Z. Ye, and S. Wang (Eds.) “Advances in Business Intelligence and Financial Engineering, Proceedings of the 2008 International Conference on Business Intelligence and Financial Engineering (BIFE 2008), October 28-30, 2008, Changsha, China,” Advances in Intelligent Systems Research, Vol. 5, pp. 21-27, Atlantis Press, October 2008. 

[33] J. Cheng, “A Temporal Relevant Logic Approach to Modeling and Reasoning about Epistemic Processes” (Invited Paper), Proceedings of the 5th International Conference on Semantics, Knowledge and Grid, pp. 18-25, Zhuhai, China, IEEE Computer Society Press, October 2009. 

[34] J. Cheng and Y. Goto, “Representing and Reasoning about Spatial Knowledge Based on Spatial Relevant Logic,” in S. Wang, K. Tanaka, et al. (Eds.), “Conceptual Modeling for Advanced Application Domains, ER 2004 Workshops CoMoGIS, CoMWIM, ECDM, CoMoA, DGOV, and eCOMO, Shanghai, China, November 8-12, 2004, Proceedings,” Lecture Notes in Computer Science, Vol. 3289, pp. 114-126, Springer, November 2004.

[35] J. Cheng, “Spatio-temporal Relevant Logic as the Logical Basis for Specifying, Verifying, and Reasoning about Mobile Multi-agent Systems,” in S. Wang, K. Tanaka, et al. (Eds.), “Conceptual Modeling for Advanced Application Domains, ER 2004 Workshops CoMoGIS, CoMWIM, ECDM, CoMoA, DGOV, and eCOMO, Shanghai, China, November 8-12, 2004, Proceedings,” Lecture Notes in Computer Science, Vol. 3289, pp. 470-483, Springer, November 2004.

[36] J. Cheng, “Spatio-temporal Relevant Logic as the Logical Basis for Spatio-temporal Information Systems,” Proceedings of the 17th International Conference on Tools with Artificial Intelligence, pp. 270-274, Hong Kong, China, IEEE Computer Society Press, November 2005.

[37] J. Cheng, “Qualitative Spatio-temporal Reasoning about Movement of Mobile Agents/Objects,” Proceedings of the 7th International Conference on Machine Learning and Cybernetics, pp. 3341-3346, Kunming, China, The IEEE Systems, Man, and Cybernetics Society, July 2008. 

[38] J. Cheng, “Qualitative Spatio-temporal Reasoning about Moving Objects in Three-dimensional Space,” in L. Kang, et al. (Eds.), “Advances in Computation and Intelligence: Third International Symposium, ISICA 2008, Wuhan, China, December 19-21, 2008, Proceedings,” Lecture Notes in Computer Science, Vol. 5370, pp. 637–648, Springer, December 2008.

[39] T. Tagawa and J. Cheng, “Deontic Relevant Logic: A Strong Relevant Logic Approach to Removing Paradoxes from Deontic Logic,” in M. Ishizuka and A. Sattar  (Eds.), “PRICAI 2002: Trends in Artificial Intelligence, 7th Pacific Rim International Conference on Artificial Intelligence, Tokyo, Japan, August 18-22, 2002. Proceedings,” Lecture Notes in Artificial Intelligence, Vol. 2417, pp. 39-48, Springer, August 2002.

[40] J. Cheng, “Deontic Relevant Logic as the Logical Basis for Legal Information Systems,” Proceedings of the 21st Annual ACM Symposium on Applied Computing, pp. 319-320, Dijon, France, ACM Press, April 2006.

[41] J. Cheng, “Deontic Relevant Logic as the Logical Basis for Representing and Reasoning about Legal Knowledge in Legal Information Systems,” in I. Lovrek, R. J. Howlett, and L. C. Jain (Eds.), “Knowledge-Based Intelligent Information and Engineering Systems, 12th International Conference, KES 2008, Zagreb, Croatia, September 3-5, 2008, Proceedings, Part II,” Lecture Notes in Artificial Intelligence, Vol. 5178, pp. 517-525, Springer, September 2008.

[42] J. Cheng, “Temporal Deontic Relevant Logic as the Logical Basis for Decision Making Based on Anticipatory Reasoning,” Proceedings of the 2006 IEEE Annual International Conference on Systems, Man, and Cybernetics, pp. 1036-1041, Taipei, Taiwan, China, The IEEE Systems, Man, and Cybernetics Society, October 2006.

[43] J. Cheng, “Strong Relevant Logic as the Universal Basis of Various Applied Logics for Knowledge Representation and Reasoning,” in Y. Kiyoki, J. Henno, H. Jaakkola, and H. Kangassalo (Eds.), “Information Modelling and Knowledge Bases XVII,” Frontiers in Artificial Intelligence and Applications, Vol. 136, pp. 310-320, IOS Press, February 2006.

[44] 程京德, “现代逻辑之未来 – 从相关逻辑到量子逻辑，” 微信公众号“数理逻辑与哲学逻辑”，2023年7月25日。 

[45] J. Cheng, “EnCal: An Automated Forward Deduction System for General-Purpose Entailment Calculus,” in N. Terashima and E. Altman (Eds.), “Advanced IT Tools, IFIP World Conference on IT Tools, 2-6 September 1996, Canberra, Australia, IFIP ’96 -14th World Computer Congress,” pp. 507-514, Chapman & Hall, September 1996.

[46] J. Cheng, S. Nara, and Y. Goto, “FreeEnCal: A Forward Reasoning Engine with General-Purpose,” in B. Apolloni, R. J. Howlett, and L. C. Jain (Eds.), “Knowledge-Based Intelligent Information and Engineering Systems, 11th International Conference, KES 2007, Vietri sul Mare, Italy, September 12-14, 2007, Proceedings, Part II,” Lecture Notes in Artificial Intelligence, Vol. 4693, pp. 444-452, Springer, September 2007.

[47] L. Wos: “Automated Reasoning: 33 Basic Research Problem.” Prentic-Hall, 1988. 

[48] L. Wos: “The Problem of Automated Theorem Finding.” Journal of Automated Reasoning, Vol. 10, No. 1, pp. 137-138, 1993. 

[49] J. Cheng, Y. Goto, S. Nara, and T. Koh, “A Cooperative Grid Computing Approach to Automated Theorem Finding and Automated Problem Proposing,” in B. Apolloni, R. J. Howlett, and L. C. Jain (Eds.), “Knowledge-Based Intelligent Information and Engineering Systems, 11th International Conference, KES 2007, Vietri sul Mare, Italy, September 12-14, 2007, Proceedings, Part II,” Lecture Notes in Artificial Intelligence, Vol. 4693, pp. 840-851, Springer, September 2007. 

[50] H. Gao, K. Shi, Y. Goto, and J. Cheng, “Automated Theorem Finding by Forward Deduction Based on Strong Relevant Logic: A Case Study in NBG Set Theory,” Proceedings of the 11th International Conference on Machine Learning and Cybernetics, pp. 1859-1865, Xi’an, China, The IEEE Systems, Man, and Cybernetics Society, July 2012. 

[51] H. Gao, K. Shi, Y. Goto, and J. Cheng, “Finding Theorems in NBG Set Theory by Automated Forward Deduction Based on Strong Relevant Logic,” in D.-Z. Du and G. Zhang (Eds.), “Computing and Combinatorics, The 19th Annual International Conference, COCOON 2013, Hangzhou, China, June 21-23, 2013, Proceedings,” Lecture Notes in Computer Science, Vol. 7936, pp. 697-704, Springer, June 2013. 

[52] H. Gao, Y. Goto, and J. Cheng, “Automated Theorem Finding by Forward Deduction Based on the Semi-Lattice Model of Formal Theory: A Case Study in NBG Set Theory,” Proceedings of the 9th International Conference on Semantics, Knowledge and Grid, pp. 22 - 29, Beijing, China, IEEE Computer Society Press, October 2013. 

[53] H. Gao, Y. Goto, and J. Cheng, “A Systematic Methodology for Automated Theorem Finding,” Theoretical Computer Science, Vol. 554, pp. 2-21, Elsevier B.V., October 2014.  

[54] H. Gao, Y. Goto, and J. Cheng, “Explicitly Epistemic Contraction by Predicate Abstraction in Automated Theorem Finding: A Case Study in NBG Set Theory,” in N. T. Nguyen, B. Trawinski, and R. Kosala (Eds.), “Intelligent Information and Database Systems, 7th Asian Conference, ACIIDS 2015, Bali, Indonesia, March 23-25, 2015, Proceedings,” Lecture Notes in Artificial Intelligence, Vol. 9011, pp. 593-602, Springer, March 2015. 

[55] H. Gao, Y. Goto, and J. Cheng, “Automated Theorem Finding by Automated Forward Reasoning Based on Strong Relevant Logic: A Case Study in Graph Theory,” in J. J. J. H. Park, H.-C. Chao, H. Arabnia, and N. Y. Yen (Eds.), “Advanced Multimedia and Ubiquitous Engineering - Future Information Technology,” Lecture Notes in Electrical Engineering, Vol. 352, pp. 23-30, Springer, May 2015. 

[56] H. Gao and J. Cheng, “An Epistemic Programming Approach for Automated Theorem Finding,” Proceedings of the 14th IEEE International Conference on Cognitive Informatics & Cognitive Computing, pp. 49-58, Beijing, China, IEEE Computer Society Press, July 2015. 

[57] H. Gao, Y. Goto, and J. Cheng, “A Set of Metrics for Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning: A Case Study in NBG Set Theory,” in X. He, X. Gao, Y. Zhang, Z.-H. Zhou, Z.-Y. Liu, B. Fu, F. Hu, and Z. Zhang (Eds.), “Intelligence Science and Big Data Engineering. Big Data and Machine Learning Techniques, 5th International Conference, IScIDE 2015, Suzhou, China, June 14 - 16, 2015, Revised Selected Papers, Part II,” Lecture Notes in Computer Science, Vol. 9243, pp. 508-517, Springer, November 2015. 

[58] H. Gao and J. Cheng, “Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic: A Case Study in Tarski's Geometry,” in J. J. J. H. Park, H. Jin, Y. Jeong, and M. K. Khan (Eds.), “Advanced Multimedia and Ubiquitous Engineering - FutureTech & MUE,” Lecture Notes in Electrical Engineering, Vol. 393, pp. 55-61, Springer, August 2016.

[59] H. Gao and J. Cheng, “Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning: A Case Study in Peano's Arithmetic,” in N. T. Nguyen, S. Tojo, L. M. Nguyen, and B. Trawinski (Eds.), “Intelligent Information and Database Systems, 9th Asian Conference, ACIIDS 2017, Kanazawa, Japan, April 3-5, 2017, Proceedings, Part II,” Lecture Notes in Artificial Intelligence, Vol. 10192, pp. 115-124, Springer, April 2017.

[60] Y. Goto, H. Gao, and J. Cheng, “A Predicate Suggestion Algorithm for Automated Theorem Finding with Forward Reasoning,” in N. T. Nguyen, S. Tojo, L. M. Nguyen, and B. Trawinski (Eds.), “Intelligent Information and Database Systems, 9th Asian Conference, ACIIDS 2017, Kanazawa, Japan, April 3-5, 2017, Proceedings, Part II,” Lecture Notes in Artificial Intelligence, Vol. 10192, pp. 125-134, Springer, April 2017.

[61] H. Gao, J. Li, and J. Cheng, “Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning: A Case Study in Tarski's Geometry,” Proceedings of the IEEE SmartWorld 2018 – 4th IEEE Smart World Congress, pp. 168-173, Guangzhou, China, The IEEE Computer Society, October 2018.

[62] J. Cheng, “A Relevant Logic Approach to Modeling Epistemic Processes in Scientific Discovery,” Proceedings of the 3rd Pacific Rim International Conference on Artificial Intelligence, Vol. 1, pp. 444-450, Beijing, China, August 1994. 

[63] J. Cheng, “Epistemic Programming -Toward a New Programming Paradigm for Scientific Discovery,” Proceedings of the 1996 IEEE Annual International Conference on Systems, Man, and Cybernetics, Vol. 3, pp. 2400-2406, Beijing, China, The IEEE Systems, Man, and Cybernetics Society, October 1996.

[64] J. Cheng, “Epistemic Programming: What Is it and Why Study it?” in M. Li (Ed.), “New Technologies on Computer Software: Proceedings of the 1997 International Symposium of New Technologies on Computer Software, Beijing, China, September 1997,” pp. i-ix, International Academic Publishers, September 1997.

[65] J. Cheng, “Epistemic Programming: What Is It and Why Study It?” Chinese Journal of Advanced Software Research, Vol. 6, No. 2, pp. 153-163, Allerton Press, USA, June 1999. (Invited Paper)

[66] J. Cheng, “Epistemic Programming: Can We have a ‘Science’ and/or an ‘Engineering’ of Scientific Discovery in the 21st Century?” Proceedings of the 1999 IPSJ Annual Summer Symposium on Programming - The Dreams of the 21st Century, pp. 19-29, Fukushima, Japan, IPSJ, August 1999. 

[67] J. Cheng, “Programming with Conditionals: Epistemic Programming for Scientific Discovery,” Wuhan University Journal of Natural Sciences, Vol. 6, No. 1-2, Special Issue: Proceedings of the International Software Engineering Symposium 2001, pp. 326-332, Wuhan University Journals Press, Wuhan, China, March 2001.

[68] I. Takahashi, S. Nara, Y. Goto, and J. Cheng, “EPLAS: An Epistemic Programming Language for All Scientists,” in Y. Shi, G. D. v. Albada, J. Dongarra, and P. M. A. Sloot (Eds.), “Computational Science -ICCS 2007: 7th International Conference, Beijing, China, May 27-30, 2007, Proceedings, Part I,” Lecture Notes in Computer Science, Vol. 4487, pp. 406-413, Springer, May 2007.

[69] W. Fang, I. Takahashi, Y. Goto, and J. Cheng, “Practical Implementation of EPLAS: An Epistemic Programming Language for All Scientists,” Proceedings of the 10th International Conference on Machine Learning and Cybernetics, Vol. 2, pp. 608-616, Guilin, China, The IEEE Systems, Man, and Cybernetics Society, July 2011.

[70] Y. Goto and J. Cheng, “A Truth Maintenance System for Epistemic Programming Environment” (Invited Paper), Proceedings of the 8th International Conference on Semantics, Knowledge and Grid, pp. 1-8, Beijing, China, IEEE Computer Society Press, October 2012.

[71] J. Cheng, “Entailment Calculus as a Logical Tool for Reasoning Rule Generation and Verification,” in J. Liebowitz (Ed.), “Moving Towards Expert Systems Globally in the 21st Century: Refereed papers accepted and presented at the 2nd World Congress on Expert Systems, Lisbon, Portugal, January 1994,” pp. 386-392, Cognizant Communication Co. (Hardbound), Macmillan New Media (CD-ROM), March 1994. 

[72] J. Cheng, “Autonomous and Continuous Evolution of Information Systems,” in R. Khosla, R. J. Howlett, and L. C. Jain (Eds.), “Knowledge-Based Intelligent Information and Engineering Systems, 9th International Conference, KES 2005, Melbourne, Australia, September 14-16, 2005, Proceedings, Part I,” Lecture Notes in Artificial Intelligence, Vol. 3681, pp. 758-767, Springer, September 2005.

[73] R. Rosen, “Anticipatory Systems - Philosophical, Mathematical and Methodological Foundations,” 1st Edition, Pergamon, 1985, 2nd Edtion, Springer, 2012. 

[74] D. M. Dubois, “Computing Anticipatory Systems with Incursion and Hyperincursion,” in Computing Anticipatory Systems: CASYS - First International Conference, edited by D. M. Dubois, AIP Conference Proceedings 437, pp. 3-29, American Institute of Physics 1998. 

[75] J. Cheng, “Anticipatory Reasoning-Reacting Systems,” Proceedings of the International Conference on Systems, Development and Self-organization, pp. 161-165, Beijing, China, November 2002. 

[76] F. Shang and J. Cheng, “Anticipatory Agents Based on Anticipatory Reasoning,” in M. S. Hacid, N. Murray, Z. W. Ras, and S. Tsumoto (Eds.), “Foundations of Intelligent Systems, 15th International Symposium, ISMIS 2005, Saratoga Springs, USA, May 25-28, 2005, Proceedings,” Lecture Notes in Artificial Intelligence, Vol. 3488, pp. 445-455, Springer, May 2005.

[77] F. Shang, S. Nara, T. Omi, Y. Goto, and J. Cheng, “A Prototype Implementation of an Anticipatory Reasoning-Reacting System” (Invited Paper), in D. M. Dubois (Ed.), “Computing Anticipatory Systems: CASYS 2005 -Seventh International Conference, Liege, Belgium, 8-13 August 2005,” AIP Conference Proceedings, Vol. 839, pp. 401-414, American Institute of Physics, June 2006.

[78] J. Cheng, Y. Goto, and N. Kitajima, “Anticipatory Reasoning about Mobile Objects in Anticipatory Reasoning-Reacting Systems” (Invited Paper), in D. M. Dubois (Ed.), “Computing Anticipatory Systems: CASYS 2007 -Eighth International Conference, Liege, Belgium, 6-11 August 2007,” AIP Conference Proceedings, Vol. 1051, pp. 244-254, American Institute of Physics, November 2008. (Best Paper Award awarded at the Eighth International Conference on Computing Anticipatory Systems) 

[79] N. Kitajima, Y. Goto, and J. Cheng, “Development of a Decision-Maker in an Anticipatory Reasoning-Reacting System for Terminal Radar Control,” in E. Corchado, X. Wu, and E. Oja (Eds.), “Hybrid Artificial Intelligence Systems, 4th International Conference, HAIS09, Salamanca, Spain, June 10-12, Proceedings,” Lecture Notes in Artificial Intelligence, Vol. 5572, pp. 68-76, Springer, June 2009.

[80] K. Shi, Y. Goto, Z. Zhu, and J. Cheng, “Anticipatory Emergency Elevator Evacuation Systems,” in A. Selamat, N. T. Nguyen, and H. Haron (Eds.), “Intelligent Information and Database Systems, 5th Asian Conference, ACIIDS 2013, Kuala Lumpur, Malaysia, March 18-20, 2013, Proceedings, Part I,” Lecture Notes in Artificial Intelligence, Vol. 7802, pp. 117-126, Springer, March 2013. 

[81] K. Shi, Y. Goto, Z. Zhu, and J. Cheng, “Anticipatory Runway Incursion Prevention Systems,” IEICE Transactions on Information and Systems, Vol. E96-D, No. 11, pp. 2385-2396, IEICE, November 2013. 

[82] K. Wagatsuma, Y. Goto, and J. Cheng, “Formal Analysis of Cryptographic Protocols by Reasoning Based on Deontic Relevant Logic: A Case Study in Needham-Shroeder Shared-Key Protocol,” Proceedings of the 11th International Conference on Machine Learning and Cybernetics, pp. 1866-1871, Xi’an, China, The IEEE Systems, Man, and Cybernetics Society, July 2012.

[83] K. Wagatsuma, S. Anze, Y. Goto, and J. Cheng, “Formalization for Formal Analysis of Cryptographic Protocols with Reasoning Approach,” in J. J. Park, Y. Pan, C. Kim, and Y. Yan (Eds.), “Future Information Technology, FutureTech 2014,” Lecture Notes in Electrical Engineering, Vol. 309, pp 211-218, Springer, May 2014.

[84] K. Wagatsuma, Y. Goto, and J. Cheng, “A Formal Analysis Method with Reasoning for Key Exchange Protocols,” IPSJ Journal, Vol. 56, No. 3, pp. 903-910, IPSJ, March 2015 (in Japanese).

[85] K. Wagatsuma, T. Harada, S. Anze, Y. Goto, and J. Cheng, “A Supporting Tool for Spiral Model of Cryptographic Protocol Design with Reasoning-based Formal Analysis,” in “Advanced Multimedia and Ubiquitous Engineering - Future Information Technology 2,” Lecture Notes in Electrical Engineering, Vol. 354, pp. 25-32, Springer, July 2015.

[86] D. Bao, K. Wagatsuma, H. Gao, and J. Cheng, “Predicting New Attacks: A Case Study in Security Analysis of Cryptographic Protocols,” in J. J. J. H. Park, H. Jin, Y. Jeong, and M. K. Khan (Eds.), “Advanced Multimedia and Ubiquitous Engineering - FutureTech & MUE,” Lecture Notes in Electrical Engineering, Vol. 393, pp. 263-270, Springer, August 2016.

[87] J. Yan, K. Wagatsuma, H. Gao, and J. Cheng, “A Formal Analysis Method with Reasoning for Cryptographic Protocols,” Proceedings of 12th International Conference on Computational Intelligence and Security, pp. 566-570, Wuxi, China, IEEE Computer Society Press, December 2016. 

[88] J. Yan, K. Wagatsuma, H. Gao, and J. Cheng, “A Supporting Environment for Formal Analysis of Cryptographic Protocols,” in J. J. J. H. Park, S.-C. Chen, and K.-K. R. Choo (Eds.), “Advanced Multimedia and Ubiquitous Engineering – MUE/FutureTech 2017,” Lecture Notes in Electrical Engineering, Vol. 448, pp. 545-550, Springer, May 2017.

[89] J. Yan, H. Gao, and J. Cheng, “A Formal Analysis Method with Forward Reasoning for Cryptographic Protocols,” Journal of Information Security Research, Vol, 3,  No. 5, pp. 462-268, May 2017 (in Chinese). 

[90] J. Yan, S. Ishibashi, Y. Goto, and J. Cheng, “A Study on Fine-Grained Security Properties of Cryptographic Protocols for Formal Analysis Method with Reasoning,” Proceedings of the IEEE SmartWorld 2018 – 4th IEEE Smart World Congress, pp. 210-215, Guangzhou, China, The IEEE Computer Society, October 2018.

微信公众号“数理逻辑与哲学逻辑”