摘要： 自动化服务组合技术是程序生成方法在Semantic Web Services领域的一种应用。该文提取了服务的“输入”、“输出”、“前置条件”、“执行效果”、“执行功能”，定义了服务的语义5元组。通过一个转换模版，把服务描述表述成一阶谓词逻辑公式，根据“证明与程序等价”的理论，利用自动化定理证明系统，完成从已有服务到目标服务的逻辑证明，从所记录的证明路径中提取目标服务的实现体，介绍了实现这一技术的原型系统。

关键词: Web服务, 服务组合, 程序生成, 定理证明

Abstract: The automatic composition approach is an application of deductive program synthesis method in semantic Web services. The semantic of a service is defined as , which stands for “input”, “output”, “precondition”, “effect”, and “IO-vinculum” of the service. A template is used to transform this semantic into a first-order-logic formula. Based on the “proofs are programs” theory, by using an automated theorem prover, the proof from available services to object service is searched, and the implementation of the object service is extracted from the recorded proof path. A brief introduction of the prototype system is given.

Key words: Web services, service composition, program synthesis, theorem proof

中图分类号: 

• TP311