A knowledge base collected by knowledge acquisition may have redundancy, inconsistency, and incompleteness. These defects make it necessary to improve the knowledge base into a form of high-quality.
In this thesis, we propose algorithms removing redundancy and checking consistency to produce a high quality knowledge base. Redundancy removing and consistency checking of a collected knowledge base used theorem proving inference rules with two assumptions such that removing and checking would be executed non-real time for systematic and complete checking, and quality of knowledge under a knowledge representation would be invarient.
Well-defined and completeness-proved theories in theorem proving are well matched to check a collected knowledge base. And we can process a knowledge base using equality such that an object may have more than one names.