Sabemos por el teorema de Church que determinar la satisfacción de primer orden es indecidible en general, pero existen varias técnicas que podemos usar para determinar la satisfacción de primer orden. Lo más obvio es buscar un modelo finito. Sin embargo, hay una serie de declaraciones en la lógica de primer orden que podemos demostrar que no tienen modelos finitos. Por ejemplo, cualquier dominio en el que opera una función inyectiva y no sobreyectiva es infinito.
¿Cómo demostramos la satisfacción de las declaraciones de primer orden cuando no hay modelos finitos o se desconoce la existencia de modelos finitos? En la demostración automatizada de teoremas podemos determinar la satisfacción de varias maneras:
- Podemos negar la oración y buscar una contradicción. Si se encuentra uno, demostramos la validez de primer orden de la declaración y, por lo tanto, la satisfabilidad.
- Usamos saturación con resolución y nos quedamos sin inferencias. Más a menudo que no, tendremos una cantidad infinita de inferencias para hacer, por lo que esto no es confiable.
- Podemos usar el forzamiento, que supone la existencia de un modelo y también la consistencia de la teoría.
No conozco a nadie que implemente el forzamiento como una técnica mecanizada para la prueba automatizada de teoremas, y no parece fácil, pero me interesa si se ha hecho o se ha intentado, ya que se ha utilizado para demostrar la independencia de varias declaraciones. en teoría de conjuntos, que en sí misma no tiene modelos finitos.
¿Existen otras técnicas conocidas para buscar la satisfacción de primer orden que sean aplicables para el razonamiento automatizado o alguien ha trabajado en un algoritmo de forzado automatizado?
Respuestas:
Aquí hay un enfoque divertido de Brock-Nannestad y Schürmann:
Verdaderas abstracciones monádicas
La idea es tratar de traducir oraciones de primer orden en lógica monádica de primer orden , "olvidando" algunos de los argumentos. Ciertamente, la traducción no está completa : hay algunas oraciones consistentes que se vuelven inconsistentes después de la traducción.
Sin embargo, la lógica monádica de primer orden es decidible . Por lo tanto, se puede verificar si la traducción de una fórmula F es consistente:F¯¯¯¯ F
puede verificarse mediante un procedimiento de decisión e implica
Lo que implica que tiene un modelo, según el teorema de integridad.F
Este tema puede aplicarse de manera algo más general: identifique una sublógica decidible de su problema, luego traduzca su problema en él, de una manera que conserve la verdad. En particular, los solucionadores SMT modernos como Z3 se han vuelto sorprendentemente buenos para demostrar la satisfacción de las fórmulas con cuantificadores (por defecto , pero pueden funcionar bien en las fórmulas ). Π 0 2Σ01 Π02
Forzar parece estar muy lejos del alcance de los métodos automatizados en la actualidad.
fuente