The purpose of knowledge acquirement is to reveal a general association system of the scope, which helps reasoning in similar cases. The precondition for the knowledge-using phase is to be able to determine which part of it is usable; and to apply the acquired information in the new situation if so.
Proper knowledge representation is needed in order to do this effectively. Essential requirement of knowledge representation is the ability to conrm the validity and completeness of the reused knowledge derived from the original source. Since it could cause a conceptional fault to include false information or size up the result of a situation inadequately. It needs formal knowledge representation to analyze these problems with mathematical methods.
Ontologies are widely used in knowledge representation. The basic way of model verication, regardless of the represented knowledge, is to check the consistency and completeness of the ontology. An additional option is to prove the validity of some statement with a known truth value, using only the information represented in the model. In general, reasoners are used to make such logical examinations.
The range of examinations they can make is not satisfy the requirements of applications in computer science in all cases, mainly because the complexity of questions they can handle is limited.
Ontologies can be mapped to the input of tools solving satisability problems widely used to analyze the most complex technical problems.
This thesis investigates the nature and diculty of proving that SAT solvers can do in ontology reasoning. It describes an ontology-SAT mapping and its implemetation, which links the Protégé Ontology Editor to the Z3 Solver.
This system is able to prove the validity of more complex statements than the currently used reasoners. Its usage can support the ontology building and maintenance as well. It also gives a new way to discover inconsistency taking adventage of some features of the Z3 Solver.