论文部分内容阅读
智能交通是集信息化、智能化、社会化为一体的新型复杂运输系统,充满了大量的、各种各样的、复杂的不确定性信息。为了更加合理地处理这些不确定性信息,我们需要以逻辑作为其理论基础。由于智能交通系统的复杂性,因此其中必定存在大量的语言值信息以及各种软件系统。所以,基于逻辑自动推理处理其中的不可比较性、语言值信息及相应软件系统的正确性,是其前沿基础研究方向之一。格值逻辑是一种重要的多值逻辑,它能同时刻画可比较性信息和不可比较性信息。本文的主要工作是在基于格蕴涵代数的格值逻辑系统中建立基于分层归结原理的自动推理方法,并进一步在基于语言真值格蕴涵代数的语言真值格值逻辑中分析相应的归结自动推理方法,同时构造相应的归结自动推理算法。主要有：在基于Lukasiewicz蕴涵代数Ln的格值命题逻辑LnP(X)中,给出了所有次正则与非次正则3阶不可分极简式的形式,进而得到了LnP(X)中所有3阶不可分极简式的形式,并在此基础上分析了一类3阶不可分极简式分别与0、1、2、3阶不可分极简式之间的α-可归结性。在基于语言真值格蕴涵代数Lv(n×2)的语言真值格值逻辑中分析了α-归结原理的一般形式。不失一般性,在格值命题逻辑(Ln×L2)P(X)中,将α-归结原理的一般形式等价转化为了格值命题逻辑LnP(X)中α-归结原理的一般形式,并指出类似的等价性在基于语言真值格值命题逻辑Lv(n×2)P(X)与￡vnP(X)的α-归结原理的一般形式间同样成立。进一步在格值一阶逻辑(L。×L2)F(X)中,将α-归结原理的一般形式等价转化为了LnP(X)中α-归结原理的一般形式,并指出类似的等价性在基于语言真值格值一阶逻辑Lv(n×2)F(X)与格值命题逻辑LvnP(X)的α-归结原理的一般形式间同样成立。在基于格蕴涵代数的格值逻辑系统中建立了α-准锁语义归结方法,并构造了相应的算法。基于α-归结原理的一般形式,在格值命题逻辑系统LP(X)中建立了α-准锁语义归结方法,证明了其可靠性与弱完备性。将基于格值命题逻辑(L。×L2)P(X)的α-准锁语义归结等价转化为了LnP(X)中的α-准锁语义归结,同时在基于语言真值格值命题逻辑Lv(n×2)P(X)与LvnP(X)的α-准锁语义归结之间得到了类似的结论,并在此基础上构造了一种基于Lv(n×2)P(X)的α-准锁语义归结算法。进一步将基于LP(X)的α-准锁语义归结方法拓展到了相应的格值一阶逻辑系统LF(X)中,并在LF(X)中建立了其可靠性与弱完备性。在格值一阶逻辑(Ln×L2)F(X)中,将满足一定条件的α-准锁语义归结等价转化为了LnP(X)中的α-准锁语义归结,并在基于语言真值格值一阶逻辑Lv(n×2)F(X)与格值命题逻辑LvnP(X)的α-准锁语义归结之间得到了类似的结论。文本还基于LF(X)构造了一种寻找逻辑公式基例的算法,并在此基础上结合基于L(n×3)P(X)的α-准锁语义归结算法,给出了一种基于Lv(n×2)F(X)的α-准锁语义归结算法。在基于格蕴涵代数的格值逻辑系统中建立了α-群准锁语义归结方法,并构造了相应的算法。基于α-归结原理的一般形式,在格值命题逻辑系统LP(X)中建立了一种α-群归结原理及其可靠性与完备性。在此基础上,提出了基于LP(X)的α-群准锁语义归结方法,并建立了其可靠性与弱完备性。进而将基于格值命题逻辑(Cn×L2)P(X)的α-群准锁语义归结等价转化为了LnP(X)中的α-群准锁语义归结,并在基于语言真值格值命题逻辑Lv(n×2)P(X)与LvnP(X)的α-群准锁语义归结之间得到了类似的结论。结合基于Lv(n×2)P(X)的α-准锁语义归结算法,给出了一种基于Lv(n×2)P(X)的α-群准锁语义归结算法。进一步将基于LP(X)的α-群归结原理、α-群准锁语义归结方法拓展到了相应的格值一阶逻辑系统LF(X)中,并分别建立了其可靠性与弱完备性。在格值一阶逻辑(Ln×L2)F(X)中,将满足一定条件的α-群准锁语义归结等价转化为了LnP(X)中的α-群准锁语义归结,并在基于语言真值格值一阶逻辑Lv(n×2)F(X)与格值命题逻辑LvnP(X)的α-群准锁语义归结之间得到了类似的结论。类似基于Lv(n×2)F(X)的α-准锁语义归结算法,给出了一种基于Lv(n×2)F(X)的α-群准锁语义归结算法。