Calculadora del método de refutación de Robinson online

¿Qué es el método de refutación de Robinson?

El método de refutación por resolución de Robinson consiste en explotar la regla de resolución de manera sistemática hasta obtener la cláusula vacía. Dicho de otra forma: en vez de intentar llegar a la conclusión, damos por hecho que es falsa y buscamos que todo reviente. El nombre es por John Alan Robinson, que lo publicó en 1965 — y no se quedó en la teoría: hoy sigue siendo el motor de inferencia de Prolog (un lenguaje de programación que razona con lógica).

Es una reducción al absurdo de toda la vida: supones que las premisas son ciertas y la conclusión falsa, y si eso te lleva a algo imposible, esa suposición no podía ser cierta. O sea, que las premisas sean ciertas y la conclusión falsa no puede pasar — y eso es justo lo que significa que el argumento sea válido.

La regla que se aplica en cada paso es la resolución, que se corresponde con la tautología:

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

Literales complementarios: el único requisito

Un literal es lo más pequeño con lo que trabajamos: una variable (P) o una variable negada (¬P). Y dos literales son complementarios cuando son la misma variable pero uno aparece sin negar y el otro negado. Así de simple:

• P y ¬P sí son complementarios. También Q y ¬Q, o S y ¬S.
• P y ¬Q no lo son: son variables distintas, no tienen nada que ver.
• P y P tampoco: los dos son positivos, no se contradicen en nada.

Ese es el único permiso que necesitas para dar un paso. Si un literal está en una cláusula y su complementario en otra, puedes resolverlas: tachas ese par y juntas en una sola cláusula todo lo que quedaba a los lados. Lo que sale se llama resolvente.

A la variable que se cancela se le llama pivote (aquí, P). Y una advertencia: se cancela un solo par por paso, aunque encuentres dos. Si tachas dos a la vez el resultado deja de ser correcto, y es el fallo más típico en los exámenes.

¿Por qué vale este paso? Míralo con el ejemplo de arriba. P solo puede ser verdadera o falsa. Si es verdadera, la cláusula (2) obliga a que se cumpla R. Si es falsa, la (1) obliga a que se cumpla Q. Pase lo que pase acabamos con Q ∨ R: por eso el resolvente es seguro.

Las tres formas que toma el paso

El mecanismo es siempre ese, pero según el tamaño de las cláusulas que combinas el paso recibe un nombre u otro. Son estas tres, y no hay más:

Por eso en la demostración de la calculadora verás unas líneas etiquetadas como «Resolución» y otras como «Silogismo disyuntivo»: es exactamente la misma operación, nombrada según el caso en que caiga. Si en un examen las escribes todas como «resolución» no estás diciendo nada falso, pero afinar el nombre suele puntuar.

Cláusulas y la cláusula vacía

Ya tienes lo que es un literal. Faltan dos piezas, y con ellas se puede trabajar:

• Cláusula: una disyunción de un número finito de literales, como P ∨ ¬Q ∨ R. Todo unido por «o», nada más. Una cláusula de un solo literal se llama unitaria.
• Cláusula vacía (□): la que se queda sin ningún literal. Aparece al resolver dos cláusulas unitarias complementarias, por ejemplo R y ¬R: se cancela el par y no queda nada a los lados.

¿Y por qué es tan importante llegar a □? Porque una cláusula se lee como «al menos uno de estos literales es verdadero». Si no queda ninguno, no hay forma de que sea verdadera: la cláusula vacía es siempre falsa. Y como cada resolvente es consecuencia lógica de las cláusulas de las que sale, obtener □ significa que el conjunto de partida era insatisfacible: premisas más conclusión negada no pueden ser verdaderas a la vez.

Eso es justo lo que queríamos demostrar. Por eso la cláusula vacía es el final del ejercicio, y por eso este método es completo: si el argumento es válido, la resolución siempre acaba encontrando □.

Cómo resolver un ejercicio paso a paso

El procedimiento es siempre el mismo y no hay que adivinar nada:

Paso 1 · Identificar las premisas y la conclusión

Separa las hipótesis de la tesis. Si el enunciado te da una sola fórmula A → B y te pide probar que es una tautología, la parte izquierda hace de premisas y la derecha de conclusión.

Paso 2 · Pasar las premisas a forma normal conjuntiva

Elimina los conectivos que no sean ¬, ∨ y ∧ (recuerda que A → B ≡ ¬A ∨ B), empuja las negaciones hacia dentro con las leyes de De Morgan y la doble negación, y reparte con la distributiva. Si necesitas repasarlo, tienes la calculadora de FNC paso a paso. Cada conjunción se parte en cláusulas independientes y se numeran.

Paso 3 · Negar la conclusión y añadirla como una hipótesis más

Este es el paso que define el método. La conclusión no es la meta: se niega, se pasa también a FNC y sus cláusulas se meten en la misma lista que las de las premisas. A partir de aquí todo son cláusulas, sin distinguir de dónde vienen.

Paso 4 · Resolver de forma sistemática

Busca dos cláusulas con un literal complementario, cancélalo y añade el resolvente a la lista con su número y la regla aplicada. Si el resolvente que sale es una tautología (tiene una variable y su negación a la vez) o es una cláusula que ya tenías, ni lo apuntes: sáltatelo y sigue, porque no te va a llevar a ningún sitio. Repite con las cláusulas nuevas hasta que aparezca □.

En un examen lo que nunca falla es ir por orden y probarlo todo con todo: la (1) con la (2), con la (3), con la (4)... hasta acabar esa fila; luego la (2) con la (3), con la (4)... y así hasta la última. Lo importante son las cláusulas nuevas: en cuanto sale una entra en la lista y hay que probarla con todas las demás, también con las que ya has dejado atrás. Es decir, si trabajando con la (2) te sale la (7), la pruebas con la (2), que es donde estás, pero además vuelves y la pruebas con la (1). Acabas cuando has recorrido toda la lista y ninguna pareja da nada que no tuvieras ya. Es más lento, pero es la única forma de poder afirmar que no se te ha escapado ninguna.

La calculadora hace exactamente eso cuando el argumento no es válido, para que la lista te salga en el mismo orden en que la escribirías a mano. Cuando sí hay refutación busca de otra manera, empezando por las cláusulas que vienen de la conclusión negada (la llamada estrategia del conjunto soporte), porque así la encuentra antes; y después te enseña solo los pasos que llevan a □, sin el relleno.

Paso 5 · Leer el resultado

• Llegas a la cláusula vacía □: el conjunto es insatisfacible, así que el argumento es válido (y si partías de una implicación, la fórmula es una tautología).
• Agotas todos los resolventes posibles sin llegar a la cláusula vacía □: el conjunto es satisfacible y el argumento no es válido. Existe entonces una asignación que hace verdaderas las premisas y falsa la conclusión: el contraejemplo.

Ejemplo resuelto paso a paso

Refutación de Robinson, resolución directa y reglas de inferencia

Los tres métodos resuelven el mismo tipo de ejercicio, pero no son intercambiables y conviene saber cuál te están pidiendo:

• Refutación de Robinson (esta página): se niega la conclusión y se resuelve hasta □. Es completo: si el argumento es válido, siempre acaba saliendo. Es el que se usa en Prolog y en los demostradores automáticos.
• Resolución directa: se trabaja también con cláusulas, pero sin negar nada; se derivan resolventes hasta obtener la conclusión. Más intuitivo de leer, aunque a veces no llega.
• Reglas de inferencia: se aplican modus ponens, modus tollens y los silogismos sobre las fórmulas tal cual, sin pasar por FNC. Es lo que se pide cuando el enunciado dice «usando reglas de inferencia».

Si un ejercicio se te resiste con las reglas de inferencia, pásalo por aquí: al ser un método completo, la refutación de Robinson te va a dar la demostración igualmente.

Calculadoras relacionadas

Preguntas frecuentes