Journal
INFORMATION SYSTEMS
Volume 31, Issue 4-5, Pages 340-360Publisher
PERGAMON-ELSEVIER SCIENCE LTD
DOI: 10.1016/j.is.2005.02.005
Keywords
service composition; web service; semantic web; linear logic theorem proving
Categories
Ask authors/readers for more resources
This paper introduces a method for automatic composition of Semantic Web services using Linear Logic (LL) theorem proving. The method uses a 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. LL, as a resource conscious logic, enables us to capture the concurrent features of Web services formally (including parameters, states and non-functional attributes). We use a process calculus to present the process model of the composite service. 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 complete proof. We introduce a set of subtyping rules that defines a valid dataflow for composite services. The subtyping rules that are used for semantic reasoning are presented with LL inference figures. We propose a system architecture where the DAML-S Translator, LL Theorem Prover and Semantic Reasoner can operate together. This architecture has been implemented in Java. (c) 2005 Elsevier B.V. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available