基于有向超图的命题逻辑合取范式的约简

摘要

在知识表示和自动推理领域，命题逻辑是一种极其重要的形式化语言，其中命题逻辑可满足性问题是研究最广泛的核心问题之一，约简命题逻辑公式是由SAT问题衍生的一个子问题。有向超图作为普通有向图的推广，能够恰当地表示大型超网络、数据库系统、命题逻辑等研究课题和研究领域中各元素之间的关系。以有向超图作为工具是众多的命题逻辑公式约简方法中的一种。本文基于命题逻辑和有向超图的相关知识、特别是近期的相关研究工作，主要取得了如下研究结果:
　　1、针对命题逻辑中一般的合取范式给出了与之一一对应的关联有向超图的定义，给出一种新的超路径表示方式，得到了刻画两个子句和两条超边之间的一些基本关系的等价命题和性质，为进一步利用有向超图寻找并约简具有特定的冗余结构的公式奠定了理论基础。
　　2、通过定义扩展B-图来表示霍恩公式，得到了其可满足性的若干结论及其约简性质，为进一步约简特定结构的一般公式奠定了基础。
　　3、将命题逻辑中的冗余对象分为绝对冗余变元、自归入子句、强归结子句这三类。根据两个子句归结的特点又将强归结子句分为具有R1,R2,R3结构的子句。通过研究上述冗余对象和冗余结构，得到了其约简性质，进一步在理论上证明了约简的合理性。
　　4、针对命题逻辑中五种冗余结构:绝对冗余变元、自归入子句、具有R1,R2,R3结构的强归结子句，提出了相应的约简运算，即弱尾约简、扩展的平行约简、强超边约简、强超路径约简、强连续约简，并辅以实例说明五种约简运算的正确性和有效性。

目录

声明

摘要

Abstract

CONTENTS

Chapter 1 Introduction

1．1 Research Background

1．2 Current Research Statuses

1．3 Structure of This Paper

Chapter 2 Preliminaries

2．1 CNF Formula

2．2 Directed Hypergraph

2．3 Graph Reduction Operations

2．4 Hypergraph Reduction Operations

2．5 Summary

Chapter 3 A New Directed hypergraph for CNF Formula

3．1 Representation

3．2 One-to-one Correspondence

3．3 Extended B-graph associated with Horn Formula

3．4 Summary

Chapter 4 Redundancy of CNF formula

4．1 Absolute Redundant Variable

4．2 Subsumed Clause

4．3 Clauses with Strong Resolvent

4．4 Summary

Chapter 5 New Reduction Operations

5．1 Reduction Operations

5．2 Instantiation

5．3 Summary

Conclusions and Future Work

Acknowledgments

Reference

List of Publication and Research Project