lp Manual de usuario y notas de implementaci´on F. Javier Gil Chica 2010

Parte I

Fundamentos te´ oricos 1.

Qu´ e es lp

lp es un peque˜ no programa que eval´ ua la validez de un argumento. Un argumento consta de una serie de premisas y una conclusi´on. Si la conclusi´on se sigue necesariamente de las premisas, entonces el argumento es v´alido. En caso contrario, no. Puede demostrarse que un conjunto de premisas, junto con la conclusi´on, se expresa mediante una f´ormula que puede evaluarse. Del resultado de esta evaluaci´on se sigue la validad o invalidez del argumento. El usuario introduce la f´ormula desde la l´ınea de ´ordenes y el programa ofrece el resultado.

2.

Resumen de l´ ogica de proposiciones

En esta secci´on se hace un resumen de la l´ogica de proposiciones. El resumen toma como referencia el texto de Hardgree, que puede encontrarse en la red. En cualquier caso, existen multitud de otros textos disponibles, que se recogen en la bibliograf´ıa, al final de este documento. Este resumen est´ a pensado como refresco r´ apido de conceptos que ya se estudiaron, no como texto alternativo. El lector puesto al d´ıa puede ir directamente a la parte segunda.

1

2.1.

Conceptos preliminares

La L´ogica es la ciencia del razonamiento. No se entiende aqu´ı razonamiento por los mecanismos neurofisiol´ogicos involucrados en el acto de razonar, sino por el razonamiento en s´ı mismo, y m´as concretamente, en cuanto a que sea correcto o no. La L´ogica no es una ciencia emp´ırica, sino especulativa. Se razona mediante el lenguaje, de manera que la formalizaci´on del razonamiento que hace la ciencia de la L´ogica ha de ser una formalizaci´on del lenguaje. Pero el lenguaje humano es extremadamente complejo. Por tanto, esa formalizaci´on se deber´a reducir a un subconjunto del lenguaje. En una primera restricci´on se consideran s´olo sentencias declarativas, que se definen como aquellas que pueden ser verdaderas o falsas. Sentencias que contengan interrogaciones o exclamaciones no son consideradas. En una segunda restricci´on, se consideran sentencias declarativas formadas a partir de unas pocas palabras del lenguaje com´ un. Cuando se razona, se pasa de unas verdades a otras. Definiremos un razonamiento como un conjunto de sentencias declarativas, de las cuales una de ellas se llama conclusi´on y las otras premisas. El razonamiento, que en este contexto se llama ”inferencia”, es el paso de las premisas a la conclusi´on. Hay que distinguir entre razonamientos inductivos y razonamientos deductivos. Los primeros establecen la verosimilitud de la conclusi´on, dadas las premisas. En los segundos la conclusi´on se ha de seguir necesariamente de las premisas. Las ciencias emp´ıricas razonan inductivamente. La L´ogica trata de los razonamientos deductivos. Un argumento tiene una forma y un contenido. La forma es la estructura de las sentencias: c´omo est´an hechas las sentencias, cuales son las premisas y cual la conclusi´on. El contenido es la materia sobre la cual se expresan las premisas y la conclusi´on. Un razonamiento puede ser verdadero o falso por su contenido, y verdadero o falso por su forma. Como tambi´en puede suceder que en raz´on de su contenido una sentencia no pueda decidirse si es verdadera o falsa (ej. ”Todos los cerpillos tienen cabeza cuadrada” ¿qu´e es un cerpillo? De existir ¿es verdad que tienen todos la cabeza cuadrada?) daremos la siguiente definici´on: un argumento es v´alido si la conclusi´on se sigue necesariamente de las premisas. Pues bien, el principio fundamental de la l´ogica establece que la validez de un argumento depende u ´ nicamente de su forma.

2.2.

Silogismos

La l´ogica silog´ıstica es un subconjunto de la l´ogica donde el n´ umero de premisas es exactamente dos. A su vez, las sentencias de un silogismo conectan elementos ling¨ısticos (nombres, verbos, adjetivos) mediante un reducido 2

subconjunto del lenguaje ordinario, a saber: {uno, algunos, todos, ninguno, es, no es}. Debido a su modesto alcance, los silogismos v´alidos pueden enumerarse completamente, ya que son limitados. La silog´ıstica fue inventada por Arist´oteles, y perfeccionada durante la Edad Media. Podemos escribir algunos silogismos, y ver que todos comparten la misma forma: Todos los hombres son mam´ıferos Algunos hombres no tienen pelo / Algunos mam´ıferos no tienen pelo Todos los isle˜ nos son marineros Algunos isle˜ nos no tienen aparejos / Algunos marineros no tienen aparejos etc. Se ve que ambos silogismos tienen la misma estructura: Todos los X son Y Algunos X no tienen Z / Algunos Y no tienen Z Por tanto, si este u ´ltimo silogismo es v´alido, ser´an v´alidos todos los silogismos que tengan la misma forma. Son silogismos v´alidos, como se puede comprobar f´acilmente, los siguientes Todo X es Y Todo Y es Z / Todo X es Z Todo X es Y Alg´ un X es Z / Alg´ un Y es Z Todo X es Z Ning´ un Y es Z / Ning´ un X es Y Ning´ un X es Y Alg´ un Y es Z / Alg´ un Z no es X Los s´ımbolos {X,Y,Z...} representan clases.

3

2.3.

L´ ogica de proposiciones

El nivel siguiente a la l´ogica silog´ıstica es la l´ogica de proposiciones. La l´ogica de proposiciones se ocupa de sentencias declarativas que, conectadas por elementos ling¨ u´ısticos determinados, forman nuevas sentencias declarativas: es decir, aptas para clasificarse en verdaderas o falsas. Por ejemplo, dos sentencias son ”La nieve es blanca” y ”El cielo es azul”, y otra sentencia, formada mediante la uni´on de ambas es ”La nieve es blanca y el cielo es azul”, donde el ”conector” es la palabra y. Puesto que una sentencia declarativa compuesta sigue siendo una sentencia declarativa, se sigue que pueden componerse sin l´ımite sentencias m´as complejas a partir de otras m´as simples. A sentencias declarativas compuestas como la anterior se les llama abreviadamente ”conectivas”, por la presencia de al menos un ”conector” ling¨ u´ıstico. Trataremos s´olo con conectivas llamadas ”verdaderamente funcionales”. Una conectiva es verdaderamente funcional si su cualidad de verdadera o falsa depende s´olo de la cualidad de verdaderas o falsas de las sentencias simples de que est´a compuesta. En L´ogica se prefiere hablar de verdad o falsedad no desde el punto de vista cualitativo, sino cuantitativo. Para eso, basta con asignar un valor a la cualidad de ”verdadero” y otro distinto a la cualidad de ”falso”. Por ejemplo, 0 para verdadero y 1 para falso, o cualesquiera otros. Es costumbre representar por T el valor de una sentencia verdadera y por F el valor de una sentencia falsa.

2.4.

Conectivas

El n´ umero de conectivas usadas en l´ogica de proposiciones es muy reducido, y las trataremos a continuaci´on. 1.- Conjunci´ on. La conjunci´on consiste en la conexi´on de dos sentencias mediante el elemento ling¨ u´ıstico y, como en ”La nieve es blanca y el cielo es azul”. Es costumbre en L´ogica usar s´ımbolos especiales para las conectivas y para las sentencias. La conectiva y se representa mediante ’&’ y las sentencias mediante letras may´ usculas. Una conjunci´on entonces se escribe en la forma ’R&S’. Se trata de ver que ’&’ es una conectiva verdaderamente funcional, es decir, que dados los valores de verdad de R y S est´a dado el valor de verdad de ’R&S’. Claramente, s´olo se podr´a decir que R&S es T si R es T y S es T. En cualquier otro caso, R&S es F. Puesto que R puede ser T o F y S puede ser T o F, hay cuatro combinaciones posibles, y a cada combinaci´on le corresponder´a un valor T o F para R&S. Esto se suele expresar en forma de tabla, de la siguiente forma:

4

&

T

F

T F

T F

F F

2.- Disyunci´ on. La disyunci´on se forma conectando dos sentencias mediante la part´ıcula ’o’, como en ”Hoy comemos pescado o crema de puerros”. La disyunci´on de dos sentencias R y S se representa mediante ’R ∨ S’. Pero la disyunci´on puede tener un sentido exclusivo (si R es cierto no puede serlo S, como en ”Vamos a la monta˜ na o a la playa”) y un sentido inclusivo (pueden ser ciertos simultaneamente R y S, como en ”Hoy comemos pescado o crema de puerros”). En lat´ın existen part´ıculas diferentes seg´ un que el sentido de la disyunci´on sea inclusivo (vel) o exclusivo (aut). En L´ogica se toma la disyunci´on en sentido inclusivo, con lo cual la tabla de verdad de la disyunci´on es ∨

T

T F

T T T F

F

3.- Negaci´ on. La negaci´on es una ”conectiva” particular, ya que no conecta dos t´erminos, sino que opera sobre un solo t´ermino. Sin embargo, sigue siendo verdaderamente funcional, y por eso se incluye entre las conectivas. En espa˜ nol se forma con la part´ıcula no. As´ı, la negaci´on de ”llueve” es ”no llueve”. En ingl´es hay m´as posibilidades. La tabla de verdad de la negaci´on es trivial: ∼

T

F

F

T

4.- Condicional. El condicional conecta dos sentencias usando no una sino dos palabras: si y entonces, como en ”si hace buen tiempo, entonces vamos a la monta˜ na”. Las dos sentencias reciben nombres especiales: a continuaci´on de si va el antecedente; a continuaci´on de entonces va el consecuente. La conectiva en s´ı se representa mediante el s´ımbolo →. Hay un peque˜ no problema de ambig¨ uedad con el subjuntivo. V´eanse por ejemplo las sentencias: ”si viviese en Granada, entonces estar´ıa en Andaluc´ıa” y ”si viviese en Salamanca, entonces estar´ıa en Andaluc´ıa”. Para un madrile˜ no, que ni vive en Andaluc´ıa, ni en Salamanca, ni en Granada, la 5

primera sentencia, compuesta de dos sentencias falsas, es verdadera. Pero la segunda, compuesta por dos sentencias falsas, es falsa. Est´a claro por tanto que no todas las conectivas si-entonces son verdaderamente funcionales. ¿Hay alg´ un uso de la conectiva que sea verdaderamente funcional? Y, en ese caso, ¿cu´al es su tabla de verdad? La respuesta a la primera pregunta es s´ı. En el contexto de las promesas/recompensas. Por ejemplo: ”si los pedidos siguen creciendo entonces habr´a que contratar m´as empleados”, que expresar´ıamos como ’P → E’. Es razonable decir que la conectiva es falsa si, siendo el antecedente verdadero, el consecuente es falso. En cualquier otro caso, la conectiva es verdadera. Con esto, se sigue la tabla →

T

F

T F

T T

F T

5.- Bicondicional. El bicondicional se forma mediante el conector s´ı y s´ olo s´ı. Simb´olicamente: ’R ↔ S’. La mejor forma de garantizar que es verdaderamente funcional es consider´andolo como combinaci´on de conectivas funcionales anteriores. As´ı, ’R ↔ S’ equivaldr´a a ’(R → S)&(S → R)’ 1 . Con esta definici´on, calcular la tabla es trivial:

2.5.

↔

T

F

T F

T F

F T

F´ ormulas complejas

Como una conectiva es una sentencia (conecta sentencias y el resultado es una sentencia, porque se puede decidir su valor de verdad), es claro que podemos anidar sentencias. En lugar de entrar en discusiones m´as formales, escribamos algunas f´ormulas complejas: P&Q ∼ (P & Q) (∼(P & Q) ∨ R) ∼((P ∨ Q) & (P & R)) 1

Atenci´ on a los par´entesis

6

Puesto que las conectivas se pueden ver como operadores (las tablas de verdad son equivalentes a las tablas de los operadores aritm´eticos, pero m´as sencillas), es claro que las expresiones anteriores pueden calcularse. No har´a falta insistir en la necesidad de usar par´entesis cuando sea preciso. La evaluaci´on de las expresiones anteriores se rige por los mismos principios que la evaluaci´on de expresiones aritm´eticas, y puede hacerse autom´aticamente.

2.6.

Tautolog´ıas, contradicciones y f´ ormulas contingentes

Para construir la tabla de verdad de una expresi´on es ventajoso escribir esta expresi´on en notaci´on polaca inversa (NPI), al modo en que se escribe en esta notaci´on cualquier expresi´on aritm´etica. En NPI primero se escriben los operandos, y luego los operadores. La ventaja es que se elimina la necesidad de par´entesis, y, con ayuda de una pila, la evaluaci´on de expresiones puede hacerse de forma trivial y en una sola pasada: es decir, cuando se quiere evaluar una expresi´on, el programa no necesita conocer de antemano dicha expresi´on, sino que reconoce sus elementos (operadores y operandos) a medida que los encuentra y lleva a cabo las operaciones precisas, de manera que, al llegar al final de la expresi´on, ´esta est´a ya evaluada. Las reglas son sencillas: si se encuentra un operando, se apila; si se encuentra un operador, ´este retira sus argumentos de la pila, opera, y deja en la pila el resultado. Cuando se llega al final de la expresi´on, el resultado se encuentra en la pila. En NPI la expresi´on ’2+3’ se escribe ’2 3 +’ y la expresi´on ’(2+3)/(4+5)’ se escribe ’2 3 + 4 5 + /’ 2 . La tabla siguiente muestra c´omo evoluciona la pila a medida que se eval´ ua la expresi´on ’2 3 + 4 5 + /’: 2 2

3 2 3

5 +

4 5 4

5 4 5 5

9 5 +

5/9 /

Sobre la l´ınea horizontal, cada columna es la pila en un momento dado. La secuencia de columnas va de izquierda a derecha. Bajo la l´ınea horizontal cada elemento indica un operando u operador, cuyo efecto sobre la pila se refleja arriba. Pues bien, las f´ormulas complejas se pueden evaluar de la misma forma. Por ejemplo, la f´ormula ’(P & Q) → R’ se escribe en NPI como ’P Q & R →’. Si P es T, Q es F y R es T, la pila evoluciona en la forma que recoge la tabla: 2

A los usuarios de calculadoras HP esto les resultar´ a familiar

7

- - F T T T F

F &

T F T

T →

El procedimiento es id´entico al de la evaluaci´on de una expresi´on aritm´etica, y los detalles m´as sencillos. Porque los u ´nicos valores admisibles son T y F y porque las tablas de verdad de las conectivas son mucho m´as sencillas que las tablas de sumar o multiplicar. Pues bien: la tabla de verdad de una f´ormula no es m´as que una forma conveniente de ordenar y visualizar el resultado de una f´ormula cuando se toman todas las combinaciones posibles de valores para las sentencias simples que la forman. Consideremos la f´ormula ’(P & Q) ∨ (P & R)’. Contiene tres sentencias simples y cada sentencia puede tomar dos valores, luego tenemos 2 ∗ 2 ∗ 2 = 23 = 8 combinaciones posibles. Para cada combinaci´on, evaluaremos la f´ormula. Elaboramos as´ı la siguiente tabla de verdad para la f´ormula: P T T T T F F F F

Q T T F F T T F F

R T F T F T F T F

(P & Q)∨(P & R) T T T F F F F F

Respecto a la u ´ltima columna, que recoge el resultado de evaluar la f´ormula, pueden suceder tres cosas: a) que todos los elementos sean T; b) que todos los elementos sean F y c) que haya elementos T y elementos F. Cuando ocurre a) a la f´ormula se le llama tautolog´ıa; cuando ocurre b), se le llama contradicci´ on. Cuando ocurre c), la f´ormula se llama contingente. Se sigue que la negaci´on de una tautolog´ıa es una contradicci´on, la negaci´on de una contradicci´on una tautolog´ıa y la negaci´on de una f´ormula contingente es una f´ormula contingente. Dos conceptos derivados de los anteriores son los de implicaci´on l´ogica y equivalencia l´ogica. Se dice que una f´ormula A implica l´ogicamente a una f´ormula B cuando A → B es una tautolog´ıa. Es decir, cuando A → B es siempre v´alida. Por ejemplo, las f´ormulas ’∼ P’ y ’∼ (P & Q)’ son l´ogicamente equivalentes, como se sigue de la tabla de verdad:

8

P Q T T T F F T F F

∼P → ∼(P & Q) T T T T

De la misma forma, dos f´ormulas A y B se dicen l´ogicamente equivalentes cuando A ↔ B es una tautolog´ıa. Estamos ya en condiciones de definir la validez de un argumento. Recordamos que un argumento es un conjunto de sentencias, de las cuales hay una a la que llamamos conclusi´on y al resto le llamamos premisas. Formalmente, un argumento se escribe como P;Q;R;S.../C, donde P,Q,R,... son las premisas y C es la conclusi´on. Pues bien, un argumento es v´alido si la f´ormula ’P & Q & R & ...’ implica l´ogicamente a C, es decir, si (P & Q & R & S & ...) → C es una tautolog´ıa. Dicho informalmente, un argumento P/C es inv´alido si existe alg´ un caso en que siendo ciertas las premisas la conclusi´on es falsa. Si existe un caso as´ı, la implicaci´on ’P → C’ ser´a, seg´ un la tabla para →, F, luego en la u ´ltima columna de la tabla de verdad aparecer´a una F, luego la f´ormula ’P → C’ no ser´a una tautolog´ıa, luego P no implicar´a l´ogicamente a C, luego el argumento es inv´alido. Esto es todo lo que necesitamos para entender el manejo e implementaci´on de lp.

Parte II

Manual de usuario lp es un programa que eval´ ua si un argumento es v´alido o no lo es. Para ello sigue el proceso siguiente: dado un argumento P/C, se expresa mediante la f´ormula P → C, se calcula su tabla de verdad y se ve si la f´ormula es o no es una tautolog´ıa. Si lo es, el argumento es v´alido. El programa acepta f´ormulas (la escritura de un argumento como una f´ormula es trivial) que son cadenas ascii, compuestas por las conectivas {∼,&,∨,→,↔} y sentencias simples representadas por letras may´ usculas {A, B, C,..., Z}. Al invocar al programa, aparece el inductor ’?’: el usuario teclea el argumento (f´ormula) y pulse intro. Como resultado, se imprime en pantalla la tabla de verdad. La inspecci´on visual de la u ´ltima columna revela si el argumento es v´alido o no.

9

Puesto que las cadenas de entrada son cadenas ascii, se establece la siguiente correspondencia: conectiva ascii ∼ ∼ & & ∨ | → > ↔ # No hay m´as. La siguiente tabla recoge algunos ejemplos. La primera columna contiene un argumento; la segunda, la f´ormula correspondiente: P→Q;Q→R/P→R P→Q;Q→R/P&R P→R;Q→R/(P ∨ Q)→R

((P→R)&(Q→R))→(P→R) ((P→Q)&(Q→R))→(P& R) ((P→R)&(Q→R))→(P ∨ R)→R

En una segunda tabla se representan las f´ormulas junto con las cadenas ascii que es preciso teclear: ((P→R)&(Q→R))→(P→R) ((P→Q)&(Q→R))→(P& R) ((P→R)&(Q→R))→(P ∨ R)→R

((P>Q)&(Q>R))>(P>R) ((P>Q)&(Q>R))>(P&R) ((P>R)&(Q>R))>((P|Q)>R)

As´ı, despu´es de teclear el primer ejemplo y pulsar la tecla intro se obtiene la siguiente salida: ? 0 0 0 0 1 1 1 1

((P>Q)&(Q>R))>(P>R) 0 0 1 0 1 1 1 0 1 1 1 1 0 0 1 0 1 1 1 0 1 1 1 1

Como puede verse, la u ´ltima columna contiene s´olo T (1), y por tanto la f´ormula es una tautolog´ıa, y por tanto el argumento es v´alido. Para el segundo ejemplo la salida es

10

? 0 0 0 0 1 1 1 1

((P>Q)&(Q>R))>(P&R) 0 0 0 0 1 0 1 0 1 1 1 0 0 0 1 0 1 1 1 0 1 1 1 1

La f´ormula es contingente, por tanto el argumento no es v´alido. Para el tercer ejemplo: ? 0 0 0 0 1 1 1 1

((P>R)&(Q>R))>((P|Q)>R) 0 0 1 0 1 1 1 0 1 1 1 1 0 0 1 0 1 1 1 0 1 1 1 1 luego el argumento es v´alido. El programa se abandona con la orden q.

Parte III

Notas de implementaci´ on 3.

Bucle principal El sencillo bucle principal contiene los siguientes pasos

1. Presenta un inductor 2. Lee la cadena desde stdin 3. Elimina el car´acter cr 4. Si la cadena comienza por ’q’, termina 11

5. Traduce la entrada infija a postfija 6. Calcula el tama˜ no de la tabla necesario y reserva la memoria 7. Anota a qu´e columna corresponde cada sentencia (letra) simple 8. Rellena la tabla 9. Usa los valores de cada fila para calcular la u ´ltima columna, seg´ un la f´ormula de entrada 10. Imprime la tabla completa A continuaci´on, detallo los pasos relevantes, que son del 5 al 9, inclusive.

4.

Traducci´ on de la f´ ormula

Las f´ormulas se introducen en notaci´on infija habitual, como en los ejemplos de la p´agina 10. La funci´on fgets() lee la cadena de entrada del teclado y la guarda en un buffer, y a partir de ´el se re-construye la expresi´on en otro buffer, esta vez en notaci´on postfija. En el caso del primer ejemplo de la tabla citada ser´ıa preciso generar ’PQ>RS>&PR>>’. Para generar la expresi´on postfija se usa, aparte del buffer destino, un par de pilas, de acuerdo con las reglas siguientes: 1. Las sentencias (letras) van a una pila. Los par´entesis y conectivas a otra. 2. Un ) implica que todos los operadores se traspasan de arriba abajo a la salida, hasta encontrar el par´entesis de apertura. El par´entesis de apertura se elimina. Si al finalizar esta operaci´on se encuentra todav´ıa un ∼, se traspasa tambi´en. 3. Al terminar la pasada a la expresi´on, se traspasan las conectivas que queden, de arriba abajo.

5.

Tama˜ no de la tabla

Ser´a precisa una pasada para averiguar cu´antas sentencias (letras) contiene la f´ormula. Si se encuentran n sentencias, la tabla de verdad tendr´a 2n+1 elementos, incluyendo la u ´ltima columna. La memoria se reserva din´amicamente. Cada valor T o F se representa con un car´acter. Una optimizaci´on de momento innecesaria ser´ıa usar una tabla de bits en lugar de una tabla de caracteres. 12

6.

Correspondencia entre letras y columnas

El censo de letras distintas se hace mediante un vector de caracteres, uno para cada letra: char S[26]. Cada letra indexa una posici´on. Originalmente, el vector se rellena con ceros, y cada posici´on indexada por una letra que aparece es incrementada. As´ı, las posiciones distintas de cero se corresponden con letras que aparecen. Una vez hecho esto, se recorre el vector. A la primera posici´on distinta de cero se le asigna el valor 0, a la segunda posici´on distinta de cero el valor 1, a la en´esima posici´on distinta de cero el valor n − 1. Estos valores indican la columna en la tabla de verdad que corresponde a cada letra.

7.

Relleno de la tabla

Para n letras la tabla tiene 2n filas. La idea es que la primera columna contiene 2n−1 T seguidos y el mismo n´ umero de F a continuaci´on. En la segunda n−2 columna aparecen 2 T, el mismo n´ umero de F, y luego nuevamente T’s y F’s. En cada columna, se reduce a la mitad respecto a la anterior el tama˜ no de las series, y se duplica el n´ umero de series. La funci´on rellena tabla() es obvia.

8.

Calcular cada fila

El u ´ltimo paso consiste en calcular para cada fila su valor, y a˜ nadirlo a la u ´ltima columna. La expresi´on, trasladada a postfijo, contiene s´olo letras y conectivas. Una letra indexa a S[26], y en la posici´on correspondiente se encuentra el n´ umero de columna. Se toma el valor y se apila. Los operadores simplemente toman sus operandos, que, pudiendo tener s´olo los valores T y F, indexan una tabla donde se encuentra el resultado. Por ejemplo, para la conectiva & char MA[2][2]={{0,0}, {0,1}}; As´ı, si los dos u ´ltimos elementos de la pila son T y T (1 y 1), el valor T&T no es otro que MA[1][1]. Finalmente, la tabla puede imprimirse.

13

9.

´ Ultima consideraci´ on

El programa tiene una captura elemental de errores (es un ejercicio solamente). Si la expresi´on se introdujo correctamente, el resultado ser´a correcto. Si no, el resultado no est´a determinado.

Parte IV

Bibliograf´ıa 1. Hardgree, Symbolic logic 2. Kent A. Peacock, Basic symbolic logic 3. Holly P. Hirst y Jeffry L. Hirst, A primer for Logic and Proof Otros muchos documentos pueden encontrarse en la red. Estos son los que me parecen mejores.

14