Introducción a Prover9 y Mace4
Prover9 es un Demostrador Automático de Teoremas para Lógicas de Primer Orden (también se puede utilizar con Lógica Proposicional) y Mace4 busca modelos finitos y contraejemplos. Los dos programas se pueden usar por medio de un interfaz gráfico unificado, para aprovechar el uso conjunto que se suele hacer de ambas herramientas en la resolución de problemas. Prover9 es un sucesor de Otter, un demostrador automático también creado por McCune.
La sintaxis que se debe usar para proporcionar a estos programas las fórmulas (y objetivos) viene dada por la siguiente tabla:
En la pestaña Formulas debemos introducir las fórmulas que sirven de hipótesis (en la caja Assumptions) y la fórmula que queremos probar (en la caja Goals) siguiendo el formato anterior.
Aunque admite una forma de trabajo guiada (que se puede personalizar por medio de la pestaña Prover9 Options, y también a través de directivas en el fichero de entrada), nosotros haremos uso esencialmente del modo completamente automático que trae, en el que Prover9 sigue el siguiente protocolo:
- El modo principal de inferencia usado por Prover9 es el de resolución, aplicando iteradamente resolventes simples con el fin de llegar a detectar una inconsistencia.
- Prover9 comienza realizando algunas preprocesamientos en las fórmulas de entrada para convertirlas en las forma que usa para realizar la sinferencias:
- Primero niega la fórmula objetivo.
- Entonces traslada todas las fórmulas a forma clausal.
- En algunos casos hace algunos preprocesamientos adicionales, pero no son esenciales para lo que vamos a explicar aquí.
- A partir de aquí calculará las inferencias (salvo en casos muy simples, el número de inferencias a realizar puede ser extremadamente alto).
- Si detecta una inconsistencia, para y devuelve una prueba formada por la secuencia de resoluciones que han generado esa inconsistencia, así como algunas estadísticas asociadas a la prueba encontrada.
La siguiente ventana muestra un ejemplo sencillo proposicional en el que se busca si es cierto que:
\[\{p\wedge s,\ p\rightarrow q,\ q\rightarrow r\} \models r\vee t\]
Y la prueba que Prover9 ofrece tras pulsar el botón Start:
Un ejemplo similar en Primer Orden se muestra en las siguientes figuras, donde se resuelve el problema:
\[\{\forall x (hombre(x)\rightarrow mortal(x)),\ hombre(socrates)\}\models mortal(socrates)\]
Prover9 intenta demostrar que \(\Sigma \models \varphi\) intentando probar que \(\Sigma \cup \{\neg \varphi\}\) no es satisfactible. Pero, ¿qué ocurre si Prover9 falla en este intento?, en ese caso, es posible que \(\Sigma \cup \{\neg \varphi\}\) sea satisfactible y lo ideal sería obtener un modelo que lo satisface, y ese es el papel que juega Mace4.
Mace4 busca únicamente estructuras finitas sin orden, es decir, un modelo que tiene como universo un conjunto finito (los miembros de ese universo se denotarán siempe como \(\{0,\ 1,\ \dots,\ n-1\}\) para un conjunto de tamaño \(n\)), y un conjunto de funciones y relaciones (en forma de tabla) sobre el universo, que se identifican con los símbolos de funciones y predicados que se dan en la especificación de las fórmulas introducidas. Debe notarse que solo busca modelos finitos para conjuntos de fórmulas de primer orden, aunque lo podremos utilizar para la Lógica Proposicional, considerando que los Lenguajes de Primer Orden son una extensión de ella. El método que sigue Mace4 es:
-
Para un dominio de un tamaño prefijado, se construyen todas las intancias de todas las fómrulas para ese dominio. el resultado es un conjunto de cláusulas base con igualdad.
-
Entonces, se aplica un procedimiento basado en reescritura ecuacional de base, y si se detecta satisfacibilidad, el modelo (o modelos) encontrado (s) se muestra.
Por defecto, Mace4 coienza buscando una estructura de tamaño 2 y va incrementando el tamaño de búsqueda hasta que encuentra un modelo o alcanza cierto límite prefijado.
En el siguiente ejemplo proposicional intentamos ver si es cierto que:
\[\{p\wedge s,\ p\rightarrow q,\ q\rightarrow r\} \models r\wedge t\]
Prover9, tras un breve tiempo de búsqueda (porque intervienen muy pocas variables) indica que ha terminado la búsqueda sin éxito, es decir, que no ha encontrado una inconsistencia. Lo que nos lleva a usar Mace4 para buscar un contramodelo de:
\[\{p\wedge s,\ p\rightarrow q,\ q\rightarrow r,\ \neg(r\wedge t)\}\]
Tras la ejecución de Mace4 obtenemos el siguente modelo (contraejemplo de la consecuencia buscada):
 |
 |
La figura izquierda muestra la salida directa de Mace4, mientras que la derecha muestra el resultado de usar la opción de reformateo que ofrece el programa para mostrar el modelo de forma tabular, donde es más fácil interpretar los resultados y entender por qué falla.
Veamos un ejemplo de búsqueda de contramodelos en LPO. Para ello consideremos el siguiente problema:
\[\{\forall x \exists y (R(x,y))\}\models \exists y \forall x (R(x,y))\]
De nuevo, si lo intentamos con Prover9, el sistema es incapaz de dar una demostración (no encuentra una inconsistencia) debido a que es falso. Así pues, usamos Mace4 para encontrar un contraejemplo (un modelo donde \(\forall x \exists y (R(x,y))\) es cierto, pero no se verifica \(\exists y \forall x (R(x,y))\). La ejecución de Mace4 propone el siguiente contramodelo:
 |
 |
Tal y como hicimos en el caso proposicional, la figura de la izquierda muestra la salida directa de Mace4, mientras que la de la derecha muestra el resultado de reformatear el modelo obtenido usando la opción cooked. En este caso, nos propociona un modelo con un universo formado por dos elementos \(\{0,1\}\), y una interpretación de \(R\) como: \(\{(0,0),\ (1,1)\}\) (es decir, \(R\) se verifica en esos dos pares, pero no en los pares \((0,1)\) y \((1,0)\)).