Definition (Knowledge Base Consistency Checking). Given knowledge base K as input, a decision procedure for knowledge base consistency returns “K is consistent” if there is an interpretation I such that I ⊨ K, otherwise it returns “K is inconsistent.”