Calculadora de resolución de cláusulas online

¿Qué es el método de resolución?

La resolución es una regla de inferencia: una forma segura de deducir algo nuevo a partir de lo que ya sabemos. Trabaja con cláusulas, que son fórmulas en las que todo va unido por «o» (P ∨ ¬Q ∨ R).

La idea cabe en una frase: si dos cláusulas se contradicen en un literal, ese literal se cancela y el resto se junta en una cláusula nueva, el resolvente. Se corresponde con la tautología:

(P ∨ Q) ∧ (¬P ∨ R) → (Q ∨ R)

Con un ejemplo se ve enseguida. Si sabemos que «llueve o hace viento» y también que «no llueve o hace frío», podemos concluir que «hace viento o hace frío». ¿Por qué? Porque «llueve» solo puede ser verdad o mentira: si es verdad, la segunda premisa obliga a que haga frío; si es mentira, la primera obliga a que haga viento. Pase lo que pase acabamos con Q ∨ R, así que el resolvente es seguro.

A partir de ahí, el método es directo: pasamos las premisas a cláusulas y las vamos combinando para generar cláusulas nuevas, hasta obtener la conclusión que nos piden. No hay que negar nada: la conclusión solo se escribe en forma de cláusulas para saber a qué tenemos que llegar. (Negarla y buscar una contradicción es otro método distinto, la refutación de Robinson.)

Y no todos los pasos son «resolución» a secas. Según la forma de las cláusulas que combinamos, el mismo paso tiene un nombre más concreto en la tabla de reglas: modus ponens, modus tollens, silogismo disyuntivo o silogismo hipotético. La calculadora identifica cuál es en cada línea.

Reglas de inferencia de la lógica proposicional

La resolución forma parte de un conjunto de reglas de inferencia: los pasos válidos que podemos dar para llegar a una conclusión a partir de unas premisas. Decimos que un argumento es válido cuando, siempre que todas las premisas son verdaderas, la conclusión también lo es. Estas son las más habituales:

Las dos últimas son las que más nos interesan aquí: el silogismo disyuntivo es un caso particular de la resolución (cuando una de las cláusulas es un único literal). De hecho, al trabajar con cláusulas varias de estas reglas acaban siendo casos particulares de la resolución, y por eso en la demostración paso a paso la calculadora etiqueta cada línea con el nombre concreto que le corresponde: modus ponens, modus tollens, silogismo disyuntivo, resolución…

Cómo resolver un ejercicio paso a paso

El procedimiento que seguimos es siempre el mismo:

Paso 1 · Identificar las premisas y la conclusión

Separamos las hipótesis de la tesis. Si no nos dan la conclusión aparte, sino una sola fórmula A → B, tomamos la parte izquierda A como premisas y la derecha B como conclusión.

Paso 2 · Pasar las premisas a FNC y separarlas en cláusulas

Llevamos cada premisa a su forma normal conjuntiva: quitamos los conectores que no sean ∧, ∨ y ¬, empujamos las negaciones con las leyes de De Morgan y aplicamos la distributiva. Si necesitas repasarlo, tienes la calculadora de FNC. Después numeramos las cláusulas: cuando una premisa es una conjunción como P ∧ S, la partimos en dos cláusulas independientes por simplificación.

Paso 3 · Ver a qué tenemos que llegar

La conclusión la dejamos tal cual, sin negarla: es la meta. Solo la escribimos en forma clausal para poder compararla con lo que vayamos derivando. Y si la conclusión es una conjunción como S ∧ Q, no hace falta buscarla de golpe: por la regla de conjunción basta obtener S por un lado y Q por otro, y unirlas al final.

Paso 4 · Aplicar las reglas de inferencia

Buscamos dos cláusulas con un literal complementario (una variable positiva en una y negada en la otra), las combinamos y añadimos la cláusula resultante a la lista, anotando qué regla hemos usado. Si el resultado contiene una variable y su negación a la vez, es una tautología y la descartamos. El nombre concreto que recibe cada paso —modus ponens, modus tollens, silogismo disyuntivo o hipotético— depende de la forma que tengan las cláusulas que combinamos: lo tienes todo en la tabla de reglas de arriba.

Paso 5 · Leer el resultado

Repetimos hasta que ocurra una de dos cosas:

• Obtenemos todas las cláusulas de la conclusión (o una cláusula que la implica, y entonces llegamos a ella por adición): el argumento es válido. Si la conclusión era una conjunción, las unimos en un último paso por conjunción. Y si partíamos de una implicación, la fórmula es además una tautología.
• Agotamos las combinaciones sin alcanzarla: el argumento no es válido, es decir, hay un caso en que las premisas son verdaderas y la conclusión falsa.

Ejemplo resuelto paso a paso

Calculadoras relacionadas

Preguntas frecuentes