Application of Linear Logic to Web Service Composition

摘要

In this paper, we propose a method for automated web service composition by applying Linear Logic (LL) theorem proving. We distinguish value-added web services and core service and assume that the core service is already selected by the user, but its functionality may not completely match the user's requirement. Our method enables automation of combining the core service together with a set of value-added services to solve the problem. The method uses web service languages for external presentation of atomic web services (WSDL) or composite web services (BPEL4WS), while, internally, the services are presented by extralog-ical axioms and proofs in LL (in this paper, we are focusing on the internal presentation and proofs only). LL, as the internal representation language, enables us to define some characteristics of web services formally (in particular, qualitative and quantitative constraints). Usage of LL also allows subsumption reasoning on concepts and guarantees correctness and completeness of service composition process.