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 by assuming that the core service is already selected by the user, but its functionality does not completely match the user’s requirement. Our method enables automation for 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 the services are internally presented by extralogical axioms and proofs in LL. In this paper, we are focused on the internal presentation and proof. LL, as the internal representation language, enables us to define some issues required by web service composition formally, such as qualitative and quantitative constraints plus subsumption reasoning on concepts. In addition, LL guarantees the correctness and complete...