Sabemos pelo teorema da Igreja que determinar a satisfação de primeira ordem é indecidível em geral, mas existem várias técnicas que podemos usar para determinar a satisfação de primeira ordem. O mais óbvio é procurar um modelo finito. No entanto, existem várias instruções na lógica de primeira ordem que podemos demonstrar que não possuem modelos finitos. Por exemplo, qualquer domínio no qual uma função injetiva e não-adjetiva opera é infinito.
Como demonstramos satisfação para declarações de primeira ordem, onde não existem modelos finitos ou a existência de modelos finitos é desconhecida? Na prova automatizada de teoremas, podemos determinar a satisfação de várias maneiras:
- Podemos negar a sentença e procurar uma contradição. Se um for encontrado, comprovamos a validade de primeira ordem da declaração e, portanto, a satisfação.
- Usamos saturação com resolução e ficamos sem inferências. Frequentemente, teremos uma quantidade infinita de inferências a fazer, portanto isso não é confiável.
- Podemos usar o forçamento, que pressupõe a existência de um modelo e também a consistência da teoria.
Eu não conheço ninguém implementando o forçar como uma técnica mecanizada para a prova automatizada de teoremas, e isso não parece fácil, mas estou interessado se isso foi feito ou tentado, pois foi usado para provar a independência de várias declarações na teoria dos conjuntos, que por si só não tem modelos finitos.
Existem outras técnicas conhecidas para procurar a satisfação de primeira ordem aplicáveis ao raciocínio automatizado ou alguém já trabalhou em um algoritmo de forçamento automatizado?
Respostas:
Aqui está uma abordagem divertida de Brock-Nannestad e Schürmann:
Abstrações monádicas verdadeiras
A idéia é tentar traduzir sentenças de primeira ordem em lógica monádica de primeira ordem , "esquecendo" alguns dos argumentos. Certamente a tradução não está completa : existem algumas frases consistentes que se tornam inconsistentes após a tradução.
No entanto, a lógica monádica de primeira ordem é decidível . Portanto, pode-se verificar se a tradução de uma fórmula é consistente:F¯¯¯¯ F
pode ser verificado por um procedimento de decisão e implica
O que implica que tem um modelo, pelo teorema da completude.F
Esse tema pode ser aplicado de maneira um pouco mais geral: identifique uma sub lógica lógica do seu problema e depois traduza o problema para ele, de maneira a preservar a verdade. Em particular, os solucionadores SMT modernos, como o Z3 , ficaram surpreendentemente bons em provar a satisfabilidade das fórmulas com quantificadores (por padrão , mas podem ter um bom desempenho nas fórmulas ).Σ01 Π02
Forçar parece estar longe do alcance dos métodos automatizados no momento.
fonte