首页> 中文学位 >基于格值逻辑的语言真值α-广义锁归结自动推理研究
【6h】

基于格值逻辑的语言真值α-广义锁归结自动推理研究

代理获取

目录

文摘

英文文摘

Symbols and Abbreviations

1 Introduction

1.1 Research motivation

1.1.1 General background

1.1.2 Related work

1.1.3 Objectives and problem descriptions

1.2 Contributions

1.3 Organization of the dissertation

2 Preliminaries

2.1 Linguistic truth-valued lattice implication algebras

2.2 Linguistic truth-valued lattice-valued logic

2.3 α-Resolution principle in lattice-valued logic

3 The structure of generalized literals in linguistic truth-valued lattice-valued propositional logic

3.1 Introduction

3.2 The structure of k-IESF in L6P(X)

3.2.1 The structure of 3-IESF in L6P(X)

3.2.2 The structure of 4-IESF in L6P(X)

3.2.3 An algorithm for finding k-IESFs in L6P(X)

3.3 A unified method for finding k-IESFs in Ln×2P(X)

3.4 Normal properties of generalized literals

3.5 Discussions

4 α-Lock resolution method for lattice-valued logic

4.1 Introduction

4.2 α-Lock resolution method in LP(X)

4.3 α-Lock resolution method in LF(X)

4.3.1 α-Lock resolution for LF(X)

4.3.2 The soundness and completeness of α-lock resolution in LF(X)

4.3.3 An algorithm for α-lock resolution for LF(X)

4.4 The transformation of α-lock resolution between Lv(n×z)F(X)and LnP(X)

4.5 α-Satisfiability of formulae

4.5.1 α-Satisfiability of formulae in LnP(X)

4.5.2 A universal algorithm for validating α-resolvability of formulae

4.6 Discussions

5 On compatibilities of α-lock resolution method in linguistic truth-valued lattice-valued logic

5.1 Introduction

5.2 Compatibility with generalized deleting strategy

5.2.1 α-Lock resolution with generalized deleting strategy in LnF(X)

5.2.2 An algorithm for α-lock resolution with generalized deleting strategy

5.3 Compatibility with α-linear resolution method

5.3.1 α-Linear semi-lock resolution method in LnF(X)

5.3.2 An algorithm for α-linear semi-lock resolution in LnP(X)

5.4 Compatibility with α-input resolution method

5.4.1 α-Input(α-Unit)resolution method in LnF(X)

5.4.2 The completeness of α-input(α-unit)resolution in LnF(X)

5.4.3 An algorithm for α-unit resolution method in LnP(X)

5.4.4 α-Lock resolution with α-input resolution method in LnF(X)

5.5 Discussions

6 A general form of α-generalized resolution principle for linguistic truth-valued lattice-valued logic

6.1 Introduction

6.2 α-Generalized resolution principle for Lv(n×2)P(X)

6.3 α-Generalized resolution principle for Lv(n×2)F(X)

6.3.1 The α-unsatisfiblity for a general form of the logical formula

6.3.2 The completeness for the general form of α-generalized resolution principle

6.4 The transformation of α-generalized resolution between Lv(n×2)F(X)and LnP(X)

6.5 Discussions

7 α-Generalized lock resolution method for linguistic truth-valued lattiee-valued logic

7.1 Introduction

7.2 α-Generalized lock resolution method in LP(X)

7.3 α-Generalized lock resolution method in LF(X)

7.4 Equivalent transformation of α-generalized lock resolution

7.5 An algorithm for α-generalized lock resolution LnP(X)

7.6 Discussions

8 On compatibility of α-generalized lock resolution method for linguistic truth-valued lattice-valued logic

8.1 Introduction

8.2 Compatibility with α-generalized linear resolution

8.2.1 α-Generalized linear semi-lock resolution method in LnF(X)

8.2.2 An algorithm for α-generalized linear semi-lock resolution in LnP(X)

8.3 Comparisons with α-generalized resolution methods

8.4 Discussions

Conclusions and further works

Acknowledgements

Bibliography

Appendix Ⅰ

Appendix Ⅱ

List of publications and research projects

展开▼

摘要

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

著录项

相似文献

  • 中文文献
  • 外文文献
  • 专利
代理获取

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号