Por que alguns mecanismos de inferência precisam de assistência humana, enquanto outros não?

^{Estou aprendendo sozinho os provedores de teoremas automatizados / solucionadores de SMT / assistentes de prova e postar uma série de perguntas sobre o processo, começando aqui .}

Por que os provadores automatizados de teoremas, como solucionadores de ACL2 e SMT, não precisam de assistência humana, enquanto os assistentes de prova, como Isabelle e Coq , precisam ?

^{Encontre a próxima pergunta da série aqui .}

A validade das fórmulas de ordem superior geralmente não é decidível e os espaços de pesquisa são enormes ; portanto, tudo o que você pode esperar é tentar encontrar uma prova - supondo que ela exista - enumerando de forma inteligente o espaço da prova (pense em marreta , apropriadamente chamada) mas isso é difícil. Os humanos podem tocar o oráculo, fornecendo os principais lemas para guiar a prova.

Os provadores automatizados, por outro lado, normalmente lidam apenas com (subconjuntos de) lógicas decidíveis, por exemplo, lógica proposicional ou subclasses da lógica de primeira ordem, para que possam durar muito tempo, mas você sabe que será bem-sucedido eventualmente.

Observe que existem abordagens para permitir que os assistentes de provas encontrem esses lemamas importantes, por exemplo, IsaPlanner . A ferramenta adivinha lemamas (indutivos) por enumeração e teste aleatório e, em seguida, tenta prová-los. Ao iterar o processo, muitos lemas de, por exemplo, definições típicas de tipos de dados, podem ser encontrados automaticamente.

ABC pequeno

• validade - uma fórmula é válida e contém o que você atribui às variáveis ​​livres.
• variáveis ​​livres - aquelas variáveis ​​que não são limitadas por quantificadores como e$\forall$$\exists$
• decidibilidade - uma propriedade (booleana) é (Turing) decidível se houver um algoritmo que responda "sim" ou "não" (corretamente) após um período finito de tempo.
• lógica proposicional - também lógica de ordem zero ; nenhuma quantificação permitida.
• $\forall x. P(x)$$\forall f. f(4) > 0$
• lógica de ordem superior - você pode quantificar sobre (e "construir") objetos arbitrariamente complexos, por exemplo, funções de ordem superior (funções que assumem funções).

Eu diria que a distinção clássica de "prova automatizada de teoremas" (ATP) versus "prova interativa de teoremas" (ITP) precisa ser reconsiderada. Se você usa um sistema de ITP conhecido como Isabelle / HOL hoje (Isabelle2013 de fevereiro de 2013), ele integra várias ferramentas adicionais do portfólio ATP:

• Ferramentas de prova automatizadas genéricas a bordo: ferramentas Isabelle da velha escola como faste blast(por L. Paulson) e provadores automatizados mais recentes como metis(por J. Hurd).

• ATPs externos para lógica de primeira ordem que são chamados via Sledgehammer: E prover, SPASS, Vampire. A prova encontrada é analisada para descobrir quais lemas contribuíram para ela, reduzindo 10000s para 10s e fornecendo o resultado metis.

• SMTs externos com reconstrução de prova parcial, principalmente para Z3 (por S. Boehme).

• Ferramentas para encontrar contra-exemplos de declarações não comprovadas: Nitpick / Kodkodi (J. Blanchette) e Quickcheck (L. Bulwahn).

Todo esse material automatizado faz de Isabelle um provador automatizado de teoremas?

Por fim, acho que a distinção entre "ATP" e "ITP" é apenas um tipo de "rótulo" que indica como você deseja posicionar ou "vender" seu sistema: os ATPs afirmam ser "ferramentas de botão", mas Na prática, você terá que interagir (indiretamente), fornecendo parâmetros ou dicas ou reformulando seu problema. Isso pode realmente ser bastante desafiador, devido aos longos tempos de execução que são comuns na comunidade ATP.

Por outro lado, um sistema ITP é criado para pessoas que esperam no local, com acesso meio decente a estados de prova internos, para ver o que está faltando para concluir uma prova. Um sistema ITP que agrupe as ferramentas ATP da maneira de Isabelle pode se tornar mais atraente para mais usuários e mais aplicativos, do que o ITP ou o ATP sozinho.