Some applications of non clausal deduction
Anavai Ramesh · 1995
In this thesis it is shown that by using negation normal form for representing propositional formulas, rather than clause forms such as conjunctive and disjunctive normal forms, reasoning systems that are more efficient for many classes of formulas can be built. This is due the fact that the process of converting arbitrary propositional formulas into clause forms is an expensive computational task. Algorithms for two related problems in artificial intelligence, namely computing prime implicates and implicants, and computing minimal diagnoses are developed and implemented. These algorithms use negation normal form for representing proportional formulas. These algorithms are based on dissolution, an inference rule for negation normal form. Through theoretical and experimental analysis it is shown that these algorithms are superior to many clause-based algorithms. Anti-links are defined and certain operations based on them are introduced. By performing these operations, many non-prime implicants/implicates and many non-minimal diagnoses can be eliminated without doing expensive subsumption checks. Experimental results showing significant improvements obtained by using these operations are also given. An algorithm for computing prime implicants and implicates of multiple-valued logics is also developed. This algorithm is based on signed dissolution, an inference rule for multiple-valued logics.