Current technologies for Web Services are based on syntactical descriptions and, therefore, lend themselves to only limited amount of automation. Research efforts in SemanticWeb Services, such as WSMO, try to overcome this major deficiency by providing a complete semantic description for Web Services and their related aspects. In this paper we present a logical framework which exploits such formal descriptions in order to dynamically discover Web Services that match requester goals. We consider two kinds of user goals: discovery and contracting. Based on the WSMO conceptual model, we define proof obligations that formalize the concepts of a match in these two cases.We also describe a concrete realization of this framework in the F-Logic reasoning engine FLORA-2. Such a realization requires an extension of F-Logic in order to support rule reifi-cation. With this extension, F-logic becomes a suitable framework for describing and reasoning about Semantic Web Services and their capabilities.