Reductions To CNF Formula In Propositional Logic:a Directed Hypergraph Approach

Propositional logic is a highly important formalism language in knowledge representation and automatic reasoning. As a center issue, the satisifiability problem of propositional logic has been widely studied, and the reduction of propositional logic formula is a sub-problem.Directed hypergraph is a generalization of the common directed graph, which can model relationships between elements in many projects and fields like large super-network research, database systems research, propositional logic research and so on. Directed hy-pergraph, this tool, is one of the various methods to simplify propositional logic formula. Based on the knowledge of propositional logic and directed hypergraph, especially the recent related research work, the major work in this paper includes the following aspects:1. Represent a general formula in conjunctive normal form (CNF) as a directed hypergraph and a resolution path as a hyperpath. The one-to-one correspondence between CNF formula and directed hypergraph are analyzed, some basic relationships and properties of the hyperarcs associated to clauses are obtained. All of these are the foundation for later reductions.2. To obtain reduction results of Horn formula, a new B-graph called extended B-graph is defined, and two special hyperpaths are found to judge the satisfiability which is an inspiration for the reduction problem of general formula with particular structures.3. Divide the redundant objects into absolute redundant variable, subsumed clause and clause with strong resolvent, the last one contains R1, R2, R3 structures. Several reduction properties are obtained, and the reductions are proved to be sound.4. Weak tail operation, extended parallel reduction, strong hyperedge reduction, hy-perpath reduction, and strong series operation, these five new reduction operations are put forward to delete the redundant objects we concerned. Examples assist the illustration.