Domain knowledge is one of crucial factors to get a great success in requirements elicitation of high quality. In ontology-based requirements engineering, ontology is used to express domain knowledge, so that the inconsistency of domain knowledge can be found by semantic checking. This paper purposes a new algorithm based on Tableaux algorithm to detecting and resolving inconsistencies of ontology. All kinds of consistency rules of domain knowledge are formally defined at first, and then the semantic checking algorithm is presented to resolve these inconsistencies. Finally, a case study is given to show the process and validate the usability of the algorithm.