The work included in this thesis falls within the field of automated theorem and proof is in the study, definition and development of a paradigm of linear resolution, called Resolution SL *. The reason for using the term paradigm is the fact that SL * resolution itself is not a procedure but can be understood as a form of reasoning with some parameters whose instantiation gives rise to different procedures that are appropriate for treatment of different types of problems. On the other hand, has been given the name resolution SL * because, as will be explained later, is very close to elimination and resolution of SL models (hence the first part of the name). The asterisk denotes its end wishes parametrization, so that the bodies of procedures are called SL * resolution with a letter instead of the more asterisk, as will be seen later. 
The thesis has been divided into four chapters that are briefly described below. 
The first is a brief historical introduction to the auto show, which runs from the origins of logic using formal mathematical notation early in the sixteenth century until the emergence of the most important results of the logic discovered by Herbrand, Godel, Church, etc.. There is a special emphasis in this chapter in making auto show a route from their origins in the late eighteenth century to the present, where you can see what has been the evolution of this field and what discoveries and results can be presented as the major turning points. 
The second chapter presents the linear resolution and some of its major refinements since resolution is a variation SL * SL resolution and hence linear resolution. This introduces the principle of resolution, viewing the problems of mechanization, and later refinements are two resolutions: Resolution semantics and linear resolution. In conclusion we studied the major refinements resolution linear input resolution, linear resolution with fusion, linear subsumción resolution, ordered linear resolution, and resolution MTOSS TOSS, Model Elimination, and the resolution SL system MESON. 
In the third chapter will present and discuss in depth the main contributions to the field of automatic demonstration that occurred in recent years and are close to the approximation of this work. Have included the following: the demonstrator PTTP Stickel of the system based on sequences MESON Plaisted, the demonstrator of Satchmo Manthey and Bry, the Near-Horn Prolog procedures of Loveland and others, and finally, the demonstrator of SETHEO Bibel et al. Obviously have not included all the demonstrators and procedures, but those who have been regarded as the most interesting and close to resolution SL * so that it is possible to make comparisons, so that patents are the contributions made. 
The fourth chapter presents resolution SL *. Gives the formal definition of it and introduces the concept of choice of ancestors. The choice of ancestors is the mechanism to monitor implementation of the resolution of a possible ancestor to reduce the cost of implementation and adaptation of a resolution SL * type of problem being treated. Later they are the key resolution * SL, SLT and SLP procedures. This chapter takes a particular focus on the choice of ancestors, and which is the main input resolution * SL, analyzing both the benefits associated with increased efficiency as the act of giving resolution SL * the ability to adapt dealing with the problems. Also in this chapter presents an implementation of resolution SL *, in particular the SLT procedure and results are included on an extensive set of problems in the field of automatic demonstration. In the last section of this chapter is a comparison of resolution * SL with demonstrators and closest systems, both at caractarísticas and results.