In order to find suitable web services in a large mar- ket of web services, automatic support is needed to fil- ter out web services semantically. Existing matchmaking approaches mainly consider only the types of the input and output parameters, which is not sufficient in prac- tical scenarios. In this paper, we present formalisms for modeling functional and non-functional properties ofweb services and for specifying user goals. We show how ex- pressive web service descriptions can be checked for sat- isfiability of the user goal.