论文部分内容阅读
智能交通是集信息化、智能化、社会化为一体的新型复杂运输系统,充满了大量的、各种各样的、复杂的不确定性信息,是智能信息处理的重要应用领域之一。基于格值逻辑的归结自动推理是智能信息处理领域的重要基础研究内容,对处理智能交通中的不可比较性、语言值信息及相应软硬件系统正确性的形式化验证,有重要学术意义和良好应用前景。本论文在基于格值逻辑的语言真值α-归结自动推理的基础上,提出了寻找所有κ-ESFs的统一算法和判断广义文字α-可归结性的通用方法及程序。为提高α-归结自动推理效率,提出了α-锁归结方法,证明了其可靠性与完备性,设计了通用算法,并利用Matlab语言,在机器上实现了α-锁归结自动推理。进一步地,提出了语言真值格值逻辑系统中α-广义归结原理,给出了α-广义锁归结自动推理方法、算法和程序。主要取得了如下四个方面的研究成果。1、给出了语言真值格值命题逻辑系统(Lv(n×2)P(X))中寻找所有κ-IESFs和判断广义文字是否α-可归结的通用算法与程序。具体为：给出了L6P(X)中逻辑公式的运算性质,得到了该逻辑系统中寻找所有κ-IESFs的通用方法；将该方法拓展至Lv(n×2)P(X),设计了Lv(n×2)P(X)中寻找所有κ-IESFs的通用算法；从语义角度,给出了两类典型逻辑公式F=F1→F2与F=(F1→F2)’的正规性；给出了Lv(n×2)P(X)判断广义文字是否α-可归结的通用方法与程序。2、提出了语言真值格值一阶逻辑系统(Lv(n×)F(X))中α-锁归结方法,给出了该方法的相容性,并设计了相应的算法与程序。具体为：提出了α-锁归结的概念,给出了α-锁归结的性质,可靠性与完备性,及其统一算法和程序；建立了α-锁归结在Lv(n×2)F(X)和kP(X)上的等价转化性；提出了α-输入归结和α-单元归结的概念,给出了两者间的等价性,可靠性与完备性,及其在Lv(n×2)F(X)和kP(X)上的等价转化；给出了kP(X)中逻辑公式的α-可满足性；证明了在LnF(X)中α-锁归结与广义删除策略、α-线性归结、α-输入归结和α-单元归结在一定条件下是相容的,并设计了相应的统一算法。3、提出了Lv(n×2)F(X)中α-广义归结原理。具体为：提出了Lv(n×2)F(X)中α-广义归结的概念,刻画了逻辑公式的α-不可满足性；给出了α-广义归结的可靠性与完备性；建立了α-广义归结在Lv(nr2)F(X)和LnP(X)上的等价转化性。4、提出了Lv(n×2)F(X)中α-广义锁归结,给出了该方法的相容性,并设计了相应的算法与程序。具体为：提出了α-广义锁归结的概念,给出了α-广义锁归结的性质,及其可靠性与完备性,设计了统一算法和程序；建立了α-广义锁归结在Lv(n×2)F(X)和LnP(X)上的等价转化性；证明了在LnF(X)中α-广义线性半锁归结的完备性；比较分析了α-广义线性归结、α-广义语义归结和α-广义锁归结方法的有效性、复杂性和实用性。