This thesis is a study on different approaches towards answering query via efficient plans. Efficient plans can be implemented by SQL technique, hence the application to database technology. Reformulation of query helps to limit the query expression to fully accessible database tables so that such an expression can be easily translated into an efficient plan. The approaches presented here function under their own conditions. However, they share a fundamental strategy of connecting proof with plan. The proof is an answerability proof, signifying the existence of a reformulation of the query in a certain fixed vocabulary, and the plan is an executable query extracted from the proof by interpolation technique. The classification of approaches can be based on the query answering problem that they address, or it can be based on the kind of proof they exploit. Roughly speaking, the first three chapters are devoted to the problem of ontology based query answering. Therefore the conditions under which the approach functions are those constraining the ontology and its relation to the query, especially the data model employed by the ontology, a D box data model instead of the more description-logic-conventional A box data model, which motivates the use of reformulation technique. The last two chapters can be viewed as addressing a slightly different problem at hand: query answering over restricted interface. There is no ontology here, rather restrictions on data access and the usual integrity constraints. So it is essentially still the problem of answering query in face of constraints. The technique for solving this problem has been introduced long time ago in the study of predicate logic in the form of preservation and interpolation theorems. However, its application in answering queries depends on the use of these techniques to reformulate the original query into some other query that is more manageable using database techniques. Therefore across the approaches the goal of reformulation is always an executable query, whether this executability reveals itself in a safe range executable query or a relational algebra plan. At the end of chapter five I present an algorithm for extracting a Select-Project-Joinplan from a forward chaining proof given tuple generating dependencies as constraints. Though the proof here is represented by a chase sequence, it is still an entailment proof and the plan is still extracted by interpolation.