半边图模型之构造演算

提出一个动态可增殖的多层次自组织认知系统,每个层次具有形式上一致的知识表示方法,各层的自组关联、自组聚合、归约和样本表达四个知识处理模型是实现系统自组织层次增殖的核心模型。指出若要实现层次可自组织增殖的系统,其关键是要设计一个合理的聚合归约演算系统;提出一个适用于各个层次的基于可结合半边的自组图知识表示法,先给出自组图形式化的静态定义和动态定义,然后以自组关联模型为背景给出对应的自组图构造算法。

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

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

从构造性证明中提取程序

通常情况下,我们很难确定一段给定的程序是否符合它的规范,程序提取是一种从构造性证明中提取函数式程序的机制,其构造特性很好地保证了生成程序的正确性。这就为我们提供了一种开发正确性软件的方法。本文基于对Coq中程序提取机制的研究,阐述了它的理论基础、实现机制及应用。

基于ECC的程序规范描述

介绍一种扩展的类型理论构造演算ＥＣＣ；讨论了用它表示松散语义抽象类型的程序规范的方法。然后介绍如何用函数型语言ＭＬ使这种方法得以实现。

Atomic Entailment and Atomic Inconsistency and Classical Entailment

In this paper we put forward a new solution of the well-known problem of relevant logics, i.e., we construct an atomic entailment. Hence, we construct a system of predicate calculus based on the atomic entailment. Next, we establish the definition of atomic inconsistency. The atomic inconsistency establishes an infinite class of inconsistent, but non-trivial systems. In this paper we construct the new definition of the classical entailment, into the bargain.