Date Added: Jan 2011
This paper introduces a method for automatic composition of Semantic Web services using Linear Logic (LL) theorem proving. The method uses Semantic Web service language (DAML-S) for external presentation of Web services, while, internally, the services are presented by extralogical axioms and proofs in LL. The authors use a process calculus to present the composite service formally. The process calculus is attached to the LL inference rules in the style of type theory. Thus the process model for a composite service can be generated directly from the proof.