基于通信顺序进程的计算机网络通信协议形式化描述

描述和设计计算机网络通信协议时，使用抽象的同步通信机制最为方便。但在实际中，使用异步通信机制将不可避免。基于霍尔的“通信顺序进程”和其他对通信协议描述与设计的理论研究结果，本文提出一个形式化方法。

构造演算以及它在受囿算子系统中的公理化(英文)

首先简略介绍Ｃｏｑｕａｎｄ和Ｈｕｅｔ的构造演算以及Ｐｌｏｔｋｉｎ和孙踊的受囿算子系统。然后，将构造演算在受囿算子系统中进行公理化。此公理化无需无限级（数据）类型结构。原则上，可以在原构造演算的ｔｙｐｅ空间之上引入ｋｉｎｄ空间。但是，不允许在ｋｉｎｄ上使用量词，也不允许引入ｙ：ｋｉｎｄ．从技术上说，将忠实地把构造演算翻译进受囿算子系统中去。为了能对构造演算中的Π类型受予受囿算子系统中的类型，不得不引入新的算子。举例来说，构造演算中的Πｘ：Ｍ．Ｎ可用受囿算子系统中的Πｙ．ｕ：ｔｖ来表达。其中，ｘ对应于ｙ，Ｍ对应于ｔ，以及Ｎ对应于ｕ。

耶鲁枪击案: 对非单调推理案例的分析(英文)

非单调推理多见于日常生活中。比如，无证据证实Ｂ的反面，我们得出结论Ｂ。这种逻辑在计算机科学中的知识库、超大数据库和推理库中有许多运用。本案例是著名的“耶鲁枪击案”。据此介绍非单调推理。