递归集的K-1-度上半格的格嵌入性

本文研究了递归集的K-1-度上半格的格嵌入性,证明了任一可数分配格及任一可数偏序集均可嵌入〈R_K~1(NP_K~1);≤〉的任一区间.     

模归约算法表达式自动生成算法设计与实现

多项式模归约算法是计算机代数中的基本问题之一,在编码算法和密码体制设计中有着广泛应用。基于对模归约数学基础的分析,设计了模归约算法表达式自动生成算法,只要选择实现所需的字宽w和模多项式M(x)的系数,即可自动生成对应的模规约算法表达式,为模规约算法在密码编码学中的应用提供了基础。     

一个定理证明检查器

介绍了一种新型的形式说明语言ＰＤ－Ｃａｌ,该语言具有良好的表达能力以及丰富的类型。通过对由该语言描述的定理证明过程进行类型检查,可判断该证明是否是给定定理的正确的证明。在该思想的基础上,设计并实现了ＰＤ－Ｃａｌ定理证明检查器。