本论文以Semantic Web Services(语义Web服务)的自动化组合技术为研究的中心,围绕这一主要问题,分3个部分分别分析与探讨了服务的语义、组合服务、以及自动化服务组合的方法。本论文所有的研究,都是基于服务的语义进行的。“语义”是Semantic Web Services体系中最重要的一个部分。服务被解释成一种特殊的软件组件,提取其输入参数((?)nput)、输出参数((?)utput)、前置条件((?)recondition)、执行效果((?)ffect)、以及执行功能(IO-(?)inculum)这5个要素,即(I,O,P,E,V),给出了服务作为一个整体的语义定义。以此语义定义为基础,分析了服务语义之间的关联关系,给出了“服务语义匹配”的严格的形式化定义。对服务组合演算的产物——组合服务,做了深入的分析。组合服务是一种服务执行流程,以π-Calculus为形式化描述工具,分别以数据流模型(DFM)和中心控制点模型(CCM)为视点,定义了两种表达形式。定义了基于DFM表述形式的组合服务语义积分算法(SCA),用于从组件服务的语义以及组合模型来获取组合服务的语义,这是服务验证的基础。定义了基于CCM表述形式的BPEL脚本生成规则(CCM2BPEL),用于获取可发布执行的组合服务最终形式。给出了从DFM模型到CCM模型的映射算法(DFM2CCM)。以“证明与程序的等价理论(Proof as Programs)”为依据,以“基于推理的程序生成技术(Deductive Program Synthesis)”为原型,给出了实现自动化服务组合的技术解决方案——基于逻辑定理证明的自动化服务组合技术。依照一个逻辑公式转换模板,把服务的语义(I,O,P,E,V)映射成一个一阶谓词逻辑(First-Order Logic,FOL)定理,以已有服务作为已知定理,目标服务作为待证明定理。从OWL本体库以及背景知识库中导入相关的外部语义知识,以弥合已知定理之间的语义缝隙。应用自动化定理证明引擎(Automatic Theorem Prover,ATP),获取证明结果,提取证明路径。最后利用CSEA算法,从证明路径中提取目标服务的实现体(基于DFM模型),从而构建了完整的从需求到最终结果的技术路径(Problem→Proof→DFM→CCM→BPEL)。这种“从证明到程序”的方法,保证了所得组合结果的完备性与正确性。通过一个完整的应用示例,对论文中的各个关键步骤进行了具体的说明与演示。实现了一个原型系统,用于对整套方法进行初步的可行性验证。