We present a logic-based framework that is able to model semantic e-services and to verify some of properties supporting the design and maintenance of cooperative information systems. This framework is based upon a formal foundation of the Semantic Web, as the Description Logic family, that provides an expressive specification language, allowing for complex application domains. We adopt the well-known IOPE (Input, Output, Preconditions, and Effects) paradigm for the description of e-service contracts, providing a suitable operational semantics and we are able to reason about update effects also in case of under-specified e-services, using a repair-based approach. On this base, we firstly define some basic consistency and correctness properties, and then we characterize the adequacy of an e-service to achieve a user goal as foundational task in service discovery. We present decidable checking procedures for the devised properties using a reduction technique to First-Order Logic reasoning tasks, including an analysis in terms of computational complexity.