TP(Theorem Proving) has always been one of the most central concerns of AI.The traditional idea used in TP is to try to deduce the empty clause to check satisfiability.Resolution-based TP and Extension-rule based TP are two methods based on the traditional idea in TP.A new method for knowledge compilation was proposed in this research.In this paper I will define the new method as EKCCCL(Each "K" clauses Contains Complementary Literal).EKCCCL is based on the research of Extension-rule in opposition to TP,proposed that new NP problems that can be determined in a polynomial time.This research aims to challenge the traditional idea by using the inverse of resolution.Thus,the researcher tries to deduce the set of all the maximum terms to check satisfiability.The researcher discusses knowledge compilation in propositional logic as most related papers have done.As for knowledge compilation of first-order logic bases,a preliminary investigation is shown in. |