Web Services are software services that can be advertised by providers and deployed by customers using Web technologies. This concept is currently carried further to address Web service choreography. Choreography refers to the composition of individual services to services processes that can communicate and interact with another. We propose a formal ontology framework for these Web service processes that supports the description, matching, and composition through logic reasoning techniques. The Semantic Web, based on a description logic-based knowledge representation and reasoning framework, provides the foundations. Integrating aspects from modal logics and process calculi into this framework will prove essential. Categories and Subject Descriptors D.2.2 [Software Engineering]: Software/Program Verification--Correctness proofs; D.2.12 [Software Engineering]: Interoperability--Distributed objects General Terms Design, Verification Keywords Web Services, service choreography, ontologie...