El treball inclòs en la present tesi s'emmarca dins del camp de la demostració automàtica de teoremes i consistix en l'estudi, definició i desenvolupament d'un paradigma de resolució lineal, denominat Resolució SL*. La raó per a utilitzar la denominació de paradigma residix en el fet que en si mateixa resolució SL* no és un procediment, sinó que es pot entendre com una forma de raonament amb certs paràmetres la instanciación de la qual dóna lloc a diferents procediments que són adequats per al tractament de distints tipus de problemes. D'altra banda, se li ha donat el nom de resolució SL* perquè, com posteriorment s'explicarà, està molt pròxim a Eliminació de Models i a resolució SL (d'ací la primera part del nom). L'asterisc final vol denotar el seu parametrización, de manera que els procediments instàncies de resolució SL* seran denominats amb una lletra més en compte de l'asterisc, com posteriorment es veurà.
La tesi ha sigut dividida en quatre capítols que es descriuen breument a continuació. 
En el primer es realitza una breu introducció històrica a la demostració automàtica, que va des dels orígens de la lògica amb l'ús de les primeres notacions matemàtiques formals en el segle XVI fins a l'aparició dels resultats més importants de la lògica descoberts per Herbrand, Gödel, Church, etc. Es fa un especial insistència en este capítol en la demostració automàtica realitzant un recorregut des dels seus orígens a finals del segle XVIII fins al moment actual, en el qual és possible veure quin ha sigut l'evolució d'este camp i quins descobriments i resultats es poden presentar com els principals punts d'inflexió.
En el segon capítol es presenten la resolució lineal i alguns dels seus principals refinaments, ja que resolució SL* és un variació de resolució SL i per tant de resolució lineal. Per a això s'introduïx el principi de resolució, veient els problemes de la seua mecanització, i posteriorment es veuen dos refinaments de resolució: resolució semàntica i resolució lineal. Per a concloure s'estudien els principals refinaments de resolució lineal: resolució d'entrada, resolució lineal amb fusió, resolució lineal amb subsumción, resolució lineal ordenada, resolució MTOSS i TOSS, Eliminació de Models, resolució SL i el sistema HOSTAL.
En el tercer capítol es presenten i estudien amb profunditat les principals aportacions al camp de la demostració automàtica que s'han produït en els últims anys i que estan pròximes a l'aproximació del present treball. S'han inclòs els treballs següents: el demostrador PTTP de Stickel, el sistema HOSTAL basat en seqüències de Plaisted, el demostrador SATCHMO de Manthey i Bry, els procediments Near-Horn Prolog de Loveland i altres autors i, finalment, el demostrador SETHEO de Bibel i altres autors. Òbviament no s'han inclòs tots els demostradors i procediments, però sí aquells que s'han considerat com els més interessants i pròxims a resolució SL* de manera que siga possible realitzar comparacions, de manera que queden patents les aportacions realitzades.
En el quart capítol es presenta resolució SL*. Es dóna la definició formal de la mateixa i s'introduïx el concepte fonamental d'elecció d'ancestros. L'elecció d'ancestros és el mecanisme que permet controlar l'aplicació de la resolució d'ancestro fent possible una reducció del cost de la seua aplicació i una adequació de resolució SL* al tipus de problema a tractar. Posteriorment es veuen les principals instàncies de resolució SL*, els procediments SLT i SLP. En este capítol es fa un especial insistència en l'elecció d'ancestros, ja que és la principal aportació de resolució SL*, analitzant tant els avantatges que aporta associades a l'increment de l'eficiència com el fet de dotar a resolució SL* la capacitat d'adaptar-se als problemes que tracta. També en este capítol es presenta una implementació de resolució SL*, en particular del procediment SLT, i s'inclouen resultats sobre un conjunt extens de problemes del camp de la demostració automàtica. En l'última secció d'este capítol es realitza una comparació de resolució SL* amb els demostradors i sistemes més pròxims, tant a nivell de caractarísticas com de resultats.