摘要
自动化服务组合技术是程序生成方法在Semantic Web Services领域的一种应用。该文提取了服务的"输入"、"输出"、"前置条件"、"执行效果"、"执行功能",定义了服务的语义5元组<I,O,P,E,V>。通过一个转换模版,把服务描述表述成一阶谓词逻辑公式,根据"证明与程序等价"的理论,利用自动化定理证明系统,完成从已有服务到目标服务的逻辑证明,从所记录的证明路径中提取目标服务的实现体,介绍了实现这一技术的原型系统。
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.
出处
《计算机工程》
CAS
CSCD
北大核心
2007年第18期15-17,共3页
Computer Engineering
基金
国家自然科学基金资助项目(60432010)
关键词
WEB服务
服务组合
程序生成
定理证明
Web services
service composition
program synthesis
theorem proof
