A simple heuristic for knowledge base compression

Knowledge bases are quite often represented by definite Horn Boolean formulas in conjunctive normal form (CNF), where each rule in the knowledge base corresponds to one clause in the CNF which represents the knowledge base. The set of all implicates of the CNF then represents the set of all rules which are (implicit) logical consequences of the rules (explicitly) present in the knowledge base. An important role is played by the set of all quadratic implicates which can be thought of as a directed graph on the set of proposition letters of the CNF. Every strongly connected component of this directed graph represents a class of logically equivalent proposition letters and hence all such proposition letters except one are ‘redundant’. Such a redundancy can be eliminated from the knowledge base by variable renaming.