Semantic matching is based on test cases and symbolic inference. The set of components that pass the syntactic matching all have interfaces that are type-consistent with the query. These components are passed through a set of filters defined by test cases derived from the PSDL specification. Additional test cases and additional filter passes are generated until either the set of candidates is small enough or the last new test case did not eliminate any components. At this point the remaining candidates are likely candidates for satisfying the query. The final phase consists of a set of automated theorem proving techniques that attempt to conclusively show that one of the retrieved components does satisfy the query specification. These are based on algebraic specifications, term rewrite systems, and a fast but limited inference method.