This paper proposes a method to automatically generate composite services. The function of a service is specified by its Inputs, Output, Preconditions, and Result (IOPR). These functional descriptions are translated into a first-order logic (FOL) formula. An Automatic Theorem Prover (ATP) is used to generate a proof from known services (as axioms) to the composite service (as an object formula). Based on the deductive program synthesis theory, the implementation of the composite service is extracted from the proof. The "proof to program" method used here guarantees the completeness and correctness of the result. An brief introduction of the prototype system is given. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Ye, L., & Chen, J. (2006). Automatic composition of semantic Web services - A theorem proof approach. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4185 LNCS, pp. 481–487). Springer Verlag. https://doi.org/10.1007/11836025_46
Mendeley helps you to discover research relevant for your work.