描述逻辑是一类适合于刻画静态领域知识的逻辑语言，在当前成为研究热点的语义Web中扮演着关键角色，是W3C推荐的Web本体语言OWL的逻辑基础。描述逻辑的主要特点在于具有较强描述能力的同时还具有可判定性特征，并且具有高效的推理算法和推理工具作为支撑。　　为了将描述逻辑的刻画能力从静态领域扩展到动态领域，研究者提出了描述逻辑的各种扩展形式。其中，Franz Baader教授提出的时态描述逻辑ALC-LTL将描述逻辑ALC与线性时态逻辑LTL结合了起来，同时使得可满足性问题保持在EXPTIME-完全这个级别。为了进一步发挥ALC-LTL的知识表达和推理能力。首先，需要为其设计可靠和完备的判定算法；其次，需要开发有效的推理工具；最后，需要给出一些典型的应用实例。本文基于这一思路开展研究工作，完成的工作主要如下：　　（1）针对ALC-LTL缺少有效的判定算法的现状，给出了ALC-LTL的Tableau判定算法并对其性质进行了证明。该算法首先利用相关扩展规则分别对不存在后继状态的伪状态和饱和状态进行扩展；其次删除所有的伪状态；最后删除不满足要求的饱和状态。如果能生成Tableau，则所判定的公式是可满足的，否则是不可满足的，从而实现了对ALC-LTL公式的可满足性判定。　　（2）为了能够快速准确的对ALC-LTL公式的可满足性进行判定，在ALC-LTL的Tableau判定算法基础上，开发出相应的ALC-LTL(Tableau)推理机软件。软件每次只对Tableau的一条分支进行判定，如果存在一条可满足的分支，则返回结果为该公式是可满足的；如果所判定的分支存在冲突或者可能性断言没有被实现，才对下一条分支进行判定，如果所有分支都不可满足，返回结果为该公式是不可满足的，否则返回结果为该公式是可满足的。　　（3）针对语义Web服务是对动态知识的推理，将ALC-LTL应用于语义Web服务的验证中。首先，从OWL-S中的Process Model出发，对于服务组合中每一个原子服务，将其对应的原子过程的输入、输出、前提条件、局部变量以及结果分别用ALC-LTL来刻画；其次，对组合服务进行建模，并且对其推理问题进行全面刻画，将对服务的推理问题转化为对逻辑公式的可满足性判定问题，从而实现对服务组合的可执行性以及投影问题的验证；最后对服务组合实例进行验证分析。