模态转移系统的三值逻辑模型检验

分析了现有的模型检验技术应用于模态转移系统的三值逻辑公式的模型检验中存在的问题.提出了把模态转移系统转换成Kripke结构的算法以及三值逻辑公式转换成2个二值逻辑的算法,经过转换后可用现有的模型检验技术进行模型检验.用该算法转换后,状态数、转移数和原子命题数目与原模型呈线性关系,没有增加模型检验的复杂度.     

基于不完全Kripke结构三值逻辑的模型检验

模型检验技术是形式化验证中比较成熟的技术，但随着设计系统规模的增加，状态爆炸已成为其发展的一个主要问题.为解决此问题，本文提出对系统进行抽象，建立不完全的状态模型，在此状态模型上来验证表示其属性的逻辑公式.这样一个逻辑公式的真值除了真、假外，还出现了第三种情况：未知，即在这个状态模型下无法确定其真值，需要更多的状态信息才能确定.本文还讨论了二值逻辑的模型检验技术，在此基础上给出了基于不完全状态空间的三值逻辑的模型检验算法，此算法与二值逻辑模型检验算法相比，没有带来时间复杂度的增加，最后给出了三值逻辑模型检验算法的应用.     

一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。     

一种三值逻辑的NP完全问题与判定问题

本文建立了一种三值逻辑——中介逻辑的三值语义,证明了其命题演算MP与MP的可满足问题是NP完全的且其谓词演算(带或不带等词)MF,MF与ME的判定问题是算法不可解的。     

对称三值逻辑及对称三值CMOS电路

本文从负数表示的研究引入对称三进制系统与对称三值逻辑.基于作者提出的传输函数理论,本文讨论了基本对称三值运算的CMOS电路实现,并已用计算机模拟证明它们具有正确的逻辑功能与理想的DC传输特性.基于这些基本电路单元,本文进一步设计了实现加法与乘法的两种对称三值运算单元.     

对称与非对称三值逻辑的关系

1.对称三值逻辑的基本运算 对称三值逻辑的三个基本运算可以表示成非对称三值逻辑的导出运算。     

一种基于对称三值逻辑的多值学习网络

采用对称三值逻辑的数元｛１↑－，０，１｝作为信息存储的基本单位，本文提出一种用于逼近非线性函数的多值学习网络（ＫＬＮ）。该网络由多个既关联又独立的子网络构成，而每个子网络包含一个权值存储单元组和一个阈值存储单元组。所需的数学运算仅为整数的加法和逻辑判断，因而非常简单。在此基础上，研究了具有自学习功能的多值逻辑学习控制策略。仿真结果表明ＫＬＮ对非线性函数具有良好的学习和表达能力，并对复杂非线性系统具     

一种三值逻辑电路的模拟方法

本文介绍一种三值逻辑电路的模拟方法，它是通过构造模拟三值逻辑电路的基本元件。这些元件以所构造模拟保持信号连接线作为计算对象，使模拟的各个功能由保持信号关系的过程来模拟。     

由方向乘运算实现的三值逻辑乘法器的研究

一、引言从乘数与被乘数的特性来看,乘法器有三种基本形式. 1)乘法器的乘数与被乘数都为二值函数.这种乘法器可用TTL或CMOS逻辑电路来实现. 2)乘法器的乘数与被乘数仅有一个为n值函数,另一个为任意函数. 3)乘法器的乘数与被乘数都为任意函数.原则上此种乘法器可由霍尔效应乘法器.场效应晶体管和对数元件来实现.这些器件阻抗低、温度漂移大、价格高,一般不能满足     

一类SISO系统的结构奇异值u综合

具有两个标量不确定性的结构化不确定性ＳＩＳＯ系统μ综合一般是通过闭环系统μ值的上界函数ｉｎｆσ来完成的。本文给出了这种情况下μ值及其上界函数中的Ｄ阵元素的显式表达式，从而使μ分析尤其是μ综合的计算最减少很多，并给出了应用Ｄ阵元素的显式表达式的μ综合算法和一个算例。     

Reference Constructions in the Single-conclusion Proof Logic

We propose an extension of the propositional proof logic languageby the second-order variables denoting the reference constructors(like ‘the formula which is proven by x’). The prooflogic in this weak second-order language is axiomatized viathe calculus _ref, the (Functional)Logic of Proofs with References. It is supplied with the formalarithmetical semantics: we prove that _ref is sound with respect to arithmetical interpretationsand is a conservative extension of propositional single-conclusionproof logic . Finally,we demonstrate how the language of _ref can be used as a scheme language for arithmetic and providethe corresponding proof conversion method.     

类型一阶逻辑的理论证明探讨

类型一阶逻辑在传统的一阶逻辑上,引入了类型,它是多态多类逻辑程序设计语言的理论基础,对编译系统设计与实现的进一步发展具有重要意义。论文在类型一阶逻辑的理论层面进行了探讨,引入了基本简单导出的可靠性定理和等值符号的可替换性定理,并予以证明。通过这两个定理,可以简化类型一阶逻辑理论证明中的工作量,使得将来的理论研究更加方便。     

Logic Programming and Burden of Proof in Legal Reasoning

In legal reasoning, there are a lot of interesting problems related with techniques of informatics. We propose a research field called juris-informatics to hope that we could make a great success like bio-informatics to introduce various techniques of informatics into legal domain. In this paper, we show our contributions to apply logic programing to formalizing and implementing burden of proof in legal reasoning.     

综述：一般逻辑程序的证明论语义

一般逻辑程序是知识表示的重要工具，也是非单调推理研完的领域之一。一般逻辑程序的证明论语义给出一个证明过程，对应于相应的模型论语义，同时也为模型论语义的实现提供基础。本文对一般逻辑程序的证明论研究进行综述，涉及到基于各种模型论语义的证明过程，并且对各研究在语法约束、推理方式、正确性和完备性结论及实现的情况等各方面加以比较，最后给出了此问题进一步的一些研究方向。     

Name-Passing in an Ambient-Like Calculus and Its Proof Using Spatial Logic

This paper studies a restricted version of the ambient calculus. We only allow single-threaded ambients migrating in a network of immobile ambients, exchanging payloads, and delivering them. With this restriction, we arrive at a calculus free from grave interferences. In previous works, this is only possible by sophisticated type systems.We focus on the expressiveness of the restricted calculus. We show that we can still repeat Zimmer's encoding of name-passing in our calculus. Moreover, we prove a stronger operational correspon- dence result using a novel spatial logic, which specifies spatial properties of processes invariant to process reductions.     

大线性复杂度三值自相关的二元三阶分圆序列的构造

对于一类周期为素数p,p≡1(mod 3)的二元三阶分圆序列提出了一种构造方法,确保其少自相关值及大线性复杂度。利用分圆的知识计算其自相关值,并进一步考虑序列的自相关值为三值时,素数p应满足的条件。此时p应满足p=a²+12,a为整数。当p满足此形式时,序列的线性复杂度为p-1,否则为2(p-1)/3。通过计算机实验,找出了满足所给形式的p,并能生成对应的序列集,验证了序列的自相关性及线性复杂度。新序列的线性复杂度和已有的三元三阶分圆序列的相同;和二元偶数阶分圆序列的相比,大部分相同或较优(已有的有些情况为(p-1)/2、(p+1)/2或1+(p-1)/6)。所提出的构造方法可推广至其他少自相关值、大线性复杂度的奇数阶分圆序列集的构造上。大奇数阶分圆序列的平衡性也会提高,能被较好地应用于密码与通信系统中。