Introdução à verificação lógica de primeira ordem

9

Estou tentando me ensinar diferentes abordagens à verificação de software. Eu li alguns artigos. Até onde eu aprendi, a lógica proposicional com temporal geralmente usa verificação de modelo com solucionadores SAT (em sistemas reativos contínuos), mas e a lógica de primeira ordem com temporal? Ele usa provadores de teoremas? Ou também pode usar o SAT?

Qualquer sugestão de livros ou artigos para iniciantes neste assunto é muito apreciada.

FELIPE N.
fonte
2
Antes de tudo, seja bem-vindo ao CS: SE. Embora eu não seja especialista nisso, você parece estar abordando vários tópicos ao mesmo tempo, deixando muitos buracos. Não se preocupe; Eu faço isso o tempo todo. Dê uma olhada na verificação de software , em seguida, a verificação formal , em seguida, verificação de modelo e de verificação Software Formal: Modelo Verificação e teoremas
Guy Coder

Respostas:

9

A lógica de primeira ordem é indecidível, portanto, a solução SAT não ajuda muito. Dito isto, existem técnicas para verificação de modelo limitado de fórmulas de primeira ordem. Isso significa que apenas um número fixo de objetos pode ser considerado ao tentar determinar se a fórmula é verdadeira ou falsa. Claramente, isso não está completo, mas se um contra-exemplo for encontrado, ele realmente será um contra-exemplo.

A ferramenta Alloy é uma ferramenta que permite que os modelos sejam descritos na lógica de primeira ordem (embora a sintaxe da superfície seja baseada em modelos descritos relacionalmente) e usa a verificação limitada de modelos para encontrar soluções. Um solucionador SAT é usado sob o capô. Uma extensão de liga permite modelos com caráter temporal, embora tecnicamente não suporte a lógica temporal.

Se você deseja explorar mais, por exemplo, para verificar a correção do programa, consulte as ferramentas de verificação do programa. Geralmente, elas são baseadas na lógica Hoare (para raciocinar sobre pré e pós-condições), possivelmente estendidas com a lógica de Separação (para raciocinar sobre pilhas). Essas lógicas são geralmente indecidíveis, portanto, é necessária uma certa quantidade de interação entre o ser humano e a ferramenta de verificação. Alguns exemplos de ferramentas são:

Dave Clarke
fonte
10

Depois de ler sua pergunta, a única maneira que eu pude ver e ter conhecimento suficiente para unir os tópicos foi fornecer um conjunto de artigos de alto nível que detalha a verificação de software e tenta unir a verificação de modelos e a prova de teoremas. Espero que meu comentário tenha feito isso:

Dê uma olhada na verificação de software , em seguida, a verificação formal , em seguida, verificação de modelo e de verificação Software Formal: Modelo Verificação e teoremas

Dave deu uma boa resposta, pela qual não posso fazer muito mais justiça à primeira parte da pergunta do que Dave, pois também sou novo nisso.

Como esta é sua primeira pergunta em um site da SE , a razão pela qual eu não dei uma resposta, mas um comentário é porque aqui uma resposta não pode ser apenas um conjunto de links, mas deve dar uma resposta por escrito e usar links para dar suporte à resposta; portanto, um comentário em vez de uma resposta.

Com relação a:

Qualquer sugestão de livros ou artigos para iniciantes neste assunto é muito apreciada.

Os livros que eu sugeriria e usaria são:

No momento, não posso expandir mais a prova de teoremas, porque ainda estou aprendendo os prós e contras e as diferenças de cada um, mas os que estou focando são

  • HOL Light por causa do livro de John Harrison.
  • Coq porque é baseado em Cálculo de construções
  • Isabelle porque é baseada na unificação de ordem superior.

    Esses assistentes de prova também costumam ter livros, são atuais, populares, de código aberto, mantidos e têm comunidades de suporte ativas.

Nota: usei worldcat.org para referenciar os livros, mas você pode revisá-los usando o recurso de visualização interna da Amazon.

Guy Coder
fonte
Para evitar muitas edições na resposta, colocarei as informações adicionadas como comentários e, no futuro, as agruparei na resposta. Por tentar resolver as muitas semelhanças e diferenças entre os assistentes de prova. Google para Freek Wiedijk; Acho os documentos dele bastante úteis.
Guy Coder
Muito obrigado pela sua resposta detalhada e completa. Para adicionar seus comentários aos livros e fornecer um link para o livro gratuito. Novamente, não posso agradecer o suficiente :-) #
FELIPE N.