The large-granularity Web services are a new form of Web services. In contrast to the traditional Web services, they often have more interfaces, encapsulate more complex business logics, and provide more functions etc.. However, the existing Web services composition approach cannot be fit for the kind of Web service. In order to solve the problem, we propose the notation of the inverted interface dependency and extend it to OWL-S firstly. A large-granularity Web service is regarded as a group of the inverted interface dependency. Then we propose an automatic composition approach based on the idea of proofs as programs. The main idea of the method is as follows. Specification of composition requirement is described as a proposition which can be proved by related theory. The proof can be viewed as a solution of composition specification. By the case study, the availability of the approach is approved. At last, we develop a prototype JTangComposition to implement our approach.