语义Web的发展使得其逻辑基础描述逻辑也成为研究的一个热点。描述逻辑支持推理，其推理主要涉及如下问题：概念可满足性(Concept Satisfiability)，包含关系(Subsumption)，可满足性(Satisfiabilty)，实例检测(instance Checking)；而可满足性是关键问题。用于解决可满足性的Tableau算法，在当前国外的推理机研究中发挥了重要的作用。但Tableau算法复杂性和低效率制约了其实际的应用。鉴于国内推理机研究的贫乏和当前推理机效率不高，本文将设计实现一个基于Tableau算法的推理机原型系统，作为算法优化和相关研究的起点；同时，本文将研究算法内部机制，结合并行计算研究，进行对Tableau算法基础上的推理机分布化的探索。