In order to find suitable web services in a large market of web services, automatic support is needed to filter out web services semantically. Existing matchmaking approaches mainly consider only the types of the input and output parameters, which is not sufficient in practical scenarios. In this paper, we present formalisms for modeling functional and non-functional properties of web services and for specifying user goals. We show how expressive web service descriptions can be checked for satisfiability of the user goal.