Lógica proposicional: tablas de verdad, forma clausal y resolución

«Si el sensor se activa y no hay vigilante, la alarma salta». «Es de España solo si es europeo». ¿Es lo mismo if (a < b || (a >= b && c == d)) que if (a < b || c == d)? Detrás de las tres frases está la misma pregunta: qué se puede deducir de qué. La lógica proposicional es la herramienta más sencilla para responderla, y la base de la programación lógica, la verificación de software, los circuitos digitales y buena parte de la inteligencia artificial.

​

Lo que vas a aprender

• Traducir frases del lenguaje natural a fórmulas, incluidas las que más confunden (“solo si”, “es necesario”, “a menos que”).
• Leer una fórmula con la prioridad de las conectivas y calcular su valor en una interpretación.
• Clasificar fórmulas en válidas, satisfacibles e insatisfacibles, y conjuntos en consistentes e inconsistentes.
• Decidir si un razonamiento es correcto con una tabla de verdad.
• Pasar cualquier fórmula a forma normal conjuntiva y a forma clausal.
• Demostrar un razonamiento por resolución, derivando la cláusula vacía.

​

Cómo se usa el simulador

• Con premisas y conclusión, el simulador dice si el razonamiento es correcto y, si no lo es, da un contraejemplo.
• Con una sola fórmula, la clasifica: válida, satisfacible o insatisfacible.
• Con varias fórmulas sin conclusión, dice si el conjunto es consistente.
• Las proposiciones son letras minúsculas (p, q, r, p1…). V y F son las constantes verdadero y falso.

​

Fundamentos teóricos

​

Proposiciones y conectivas

Una proposición es la unidad mínima de información de la que se puede decir si es verdadera o falsa: “llueve”, “Juan es médico”. No lo son las preguntas, las exclamaciones ni las frases cuya verdad depende de una variable (”$X$ es mayor que 3”), que pertenecen a la lógica de predicados. Las proposiciones se combinan con cinco conectivas:

​

Sintaxis y prioridad

Las fórmulas bien formadas se construyen a partir de las atómicas (las proposiciones y las constantes $V$ y $F$): si $F$ y $G$ son fórmulas, también lo son $\lnot F$, $(F \land G)$, $(F \lor G)$, $(F \to G)$ y $(F \leftrightarrow G)$. Para ahorrar paréntesis se usa una prioridad, de más a menos: $$\lnot \quad > \quad \land \quad > \quad \lor \quad > \quad \to \quad > \quad \leftrightarrow$$ Así, $\lnot p \land q \to r$ se lee $((\lnot p \land q) \to r)$. Entre conectivas del mismo nivel manda la de la izquierda: $p \to q \to r$ es $(p \to q) \to r$. El simulador escribe esos paréntesis aunque no hagan falta, porque sin ellos la fórmula se lee mal.

​

Semántica: interpretaciones y tablas de verdad

Una interpretación asigna V o F a cada proposición. Con $n$ proposiciones distintas hay $2^n$ interpretaciones. El valor de una fórmula se calcula con las tablas de las conectivas: La implicación solo es falsa en un caso: antecedente verdadero y consecuente falso. Si el antecedente es falso, la implicación es verdadera (“de lo falso se sigue cualquier cosa”). Si una interpretación hace verdadera una fórmula, es un modelo de ella; si la hace falsa, un contramodelo.

​

Clasificación de fórmulas

Toda fórmula válida es satisfacible. Las dos clases se relacionan con el principio del espejo: $$F \text{ es válida} \iff \lnot F \text{ es insatisfacible}$$ Un conjunto de fórmulas es consistente si existe una misma interpretación que las hace verdaderas a todas, e inconsistente si no existe. Cuidado: $\{p,\ \lnot p\}$ es inconsistente aunque cada fórmula, por separado, sea satisfacible.

​

Equivalencia lógica

Dos fórmulas son equivalentes, $F \equiv G$, si tienen el mismo valor en todas las interpretaciones, es decir, si $F \leftrightarrow G$ es válida. Las equivalencias que más se usan:

​

Consecuencia lógica: cuándo un razonamiento es correcto

$Q$ es consecuencia lógica de las premisas $P_1, \dots, P_n$, y se escribe $\{P_1, \dots, P_n\} \models Q$, si todo modelo común de las premisas es también modelo de $Q$. Un razonamiento es correcto cuando la conclusión es consecuencia lógica de las premisas. Hay dos formas equivalentes de comprobarlo: $$\textbf{Teorema I:}\quad \{P_1, \dots, P_n\} \models Q \iff P_1 \land \dots \land P_n \to Q \text{ es válida}$$ $$\textbf{Teorema II:}\quad \{P_1, \dots, P_n\} \models Q \iff \{P_1, \dots, P_n, \lnot Q\} \text{ es inconsistente}$$ La tabla de verdad usa el Teorema I: se buscan las filas en las que todas las premisas son verdaderas y se mira la conclusión. Si en alguna es falsa, esa fila es un contraejemplo y el razonamiento no es correcto. El método funciona siempre, pero con $n$ proposiciones hay $2^n$ filas: con 10 ya son 1024.

​

Forma normal conjuntiva y forma clausal

Un literal es una proposición o su negación; $L^c$ es su complementario ($p$ y $\lnot p$). Una fórmula está en forma normal conjuntiva (FNC) si es una conjunción de disyunciones de literales, como $(p \lor \lnot q) \land (\lnot p \lor r \lor s) \land p$. Cada disyunción es una cláusula, y el conjunto de cláusulas es la forma clausal (FC). La cláusula sin literales es la cláusula vacía $\square$, que es insatisfacible. Cualquier fórmula se puede pasar a FNC en cinco pasos, los mismos que muestra el simulador:

​

Resolución

La resolución (Robinson, 1965) usa una sola regla de inferencia, muy fácil de automatizar: $$\frac{L \lor F \qquad L^c \lor G}{F \lor G}$$ Se quita un par de literales complementarios y se junta lo que queda de las dos cláusulas: el resultado es la resolvente. Funciona porque, si $L$ es falso, tiene que ser verdad $F$, y si $L$ es verdadero, tiene que serlo $G$; en los dos casos $F \lor G$ es verdad. Para demostrar un razonamiento se trabaja por refutación, con el Teorema II:

1. Se pasan a forma clausal las premisas y la negación de la conclusión.
2. Se resuelven pares de cláusulas y se añaden las resolventes.
3. Si aparece la cláusula vacía $\square$, el conjunto es inconsistente y el razonamiento es correcto.
4. Si se han resuelto todos los pares posibles sin llegar a $\square$, el conjunto es consistente y el razonamiento no es correcto.

El simulador prueba todos los pares nivel a nivel (cada cláusula nueva contra todas las anteriores), descarta las tautologías y las cláusulas absorbidas, y al final muestra solo las resolventes que llevan a $\square$.

​

Ejemplos resueltos

​

Experimenta con el simulador

​

Errores frecuentes

• Traducir “p solo si q” como $q \to p$. Es $p \to q$.
• Pensar que $p \to q$ es falsa cuando $p$ es falsa. Solo es falsa con $p$ verdadera y $q$ falsa.
• Confundir satisfacible con válida. Que una fórmula sea verdadera en alguna fila no basta para que sea una tautología.
• Olvidar negar la conclusión antes de resolver. Si se resuelve con $Q$ en lugar de $\lnot Q$, no se está demostrando nada.
• Resolver sobre dos pares a la vez. De $p \lor q$ y $\lnot p \lor \lnot q$ no se deduce $\square$: cada resolución quita un solo par, y aquí cualquier resolvente es una tautología.
• Distribuir al revés. Para la FNC se distribuye $\lor$ sobre $\land$, no $\land$ sobre $\lor$ (eso da la forma normal disyuntiva).

​

Limitaciones

La lógica proposicional no puede hablar de objetos ni de sus propiedades. “Todos los hombres son mortales; Sócrates es hombre; luego Sócrates es mortal” es un razonamiento correcto que aquí no se puede demostrar: hacen falta los cuantificadores ($\forall$, $\exists$) de la lógica de predicados. Además, comprobar si una fórmula es satisfacible (el problema SAT) es NP-completo: no se conoce ningún método que lo haga en tiempo polinómico. La tabla de verdad crece como $2^n$ y la resolución puede generar muchísimas cláusulas. El simulador dibuja tablas de hasta 7 proposiciones y se detiene al llegar a 3000 cláusulas. Aun así, los resolvedores SAT modernos resuelven problemas industriales con millones de variables.

​

Un poco de historia

Aristóteles estudió los silogismos en el siglo IV a. C., pero la lógica como cálculo nace con George Boole, que en 1854 trató las proposiciones con las reglas del álgebra. Gottlob Frege dio en 1879 el primer sistema formal completo. En 1935 Gerhard Gentzen propuso la deducción natural, que imita cómo razonan las personas, y en 1965 John Alan Robinson inventó la resolución, pensada para que razonen las máquinas. De ella salió el lenguaje Prolog (1972), que ejecuta programas resolviendo cláusulas de Horn.

​

Preguntas frecuentes

​

Temas relacionados