Abstract: The method described in this paper is based on Loveland's MESON proof procedure of debugging a knowledge base (kb) of full first order logical rules, including true negation, disjunction, and if-and-only-if rules. It is used to query the kb and to detect redundancies and inconsistencies. Explanations are provided for each contradiction and redundancy found. Both backward and forward chainning capabilities of the system make it possible to investigate the consequences of new additions to the kb.