Dynamic Web Service Assembly Using OWL and a Theorem Prover

We present a method using semantic Web technologies to dynamically compose a chain of Web services that answers a stated information problem. Web services description language (WSDL) files that define the services are automatically examined and input and output messages are extracted. The XML schema definitions are converted to OWL ontology files. The ontologies derived from the different services are mapped/aligned to one another to identify similar concepts (classes and properties). A representation of the input and output messages and the alignment data is then fed into a theorem prover Prover9, along with an information goal. If a solution exists, the theorem prover determines how the goal can be met by proving that the goal is achievable from the axioms given by the service inputs, outputs, and alignments. The steps in the proof define the service chain. The proof is then processed and turned into a business process execution language (BPEL) document, which can then be executed by a system such as NetBeans.