Existe um sistema de prova automatizado razoável para os teoremas do TCS?

28

Suponha que eu quisesse formalizar a prova de Turing sobre o problema da parada, para que uma máquina pudesse verificá-la. Alguns dos conhecidos sistemas automatizados de prova de teoremas incluem Mizar, Coq e HOL4. Fiz o download e experimentei o Coq, mas ele não possui uma biblioteca para máquinas Turing. Eu mesmo pensei em codificar um, mas achei o tutorial ausente e o idioma difícil de entender.

Minha pergunta é: Existe um provador automatizado de teoremas que geralmente é bom em provar teoremas que envolvem máquinas de Turing? Eu consideraria esse provador de teoremas "bom" se pudesse formalizar uma prova da indecidibilidade do problema de interrupção usando bibliotecas já existentes. Eu consideraria ainda melhor se for relativamente fácil de entender. (Para constar, normalmente não tenho dificuldade com linguagens de programação.)

Obrigado,

Philip

lo.logic turing-machines software proof-assistants automated-theorem-proving Philip White
fonte
Convém verificar esta página, mas a lista não inclui o problema de parada.
Kaveh
10
Ouso dizer que você precisa persistir com algo como Coq antes que pareça natural. E você precisa estar no terminal trabalhando com problemas, em vez de ler o livro. Colocar as mãos em "Provas de Teoremas Interativos e Desenvolvimento de Programas: Coq'Art: O Cálculo de Construções Indutivas" ajudará. Tutoriais Coq: cis.upenn.edu/~bcpierce/sf e adam.chlipala.net/cpdt são muito bons (embora não sejam direcionados diretamente para o que você deseja).
Dave Clarke
5
A formalização de uma prova pode ser bastante complicada se você escolher a versão "errada" dela. Para o problema da parada, eu sugeriria provar uma versão mais geral e abstrata primeiro. Depois, você poderá provar mais tarde que as máquinas de Turing são um caso especial da versão abstrata, se você ainda quiser fazê-lo (haverá muitos detalhes tediosos sobre as máquinas de Turing, então talvez seja melhor gastar tempo fazendo outra coisa). Vou pensar em uma boa maneira de provar isso no Coq. Fiquei atento.
Andrej Bauer
5
Se você é bom em matemática e bom em programação, possui os pré-requisitos para aprender a usar um assistente de prova. Você realmente precisa tratá-lo como uma nova habilidade. (É, no entanto, muito gratificante.)
Neel Krishnaswami
Parece que a resposta para a pergunta é "não". Acho que esse sistema seria muito útil - posso solicitar que, se você formalizar as máquinas de Turing, possa pensar um pouco na equivalência de tempo polinomial?
Colin McQuillan

Respostas:

17

Aqui está uma biblioteca Isabelle / HOL contendo o teorema de Rice, que declara indecidibilidade de uma ampla gama de problemas. Como essa biblioteca modela a computabilidade por meio de funções recursivas, é necessário codificar uma máquina de Turing universal como uma função recursiva para usar esse teorema para provar indecidibilidade do problema de parada das máquinas de Turing. No entanto, as partes essenciais da prova de indecidibilidade já estão concluídas.

http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html

yhirai
fonte