lógica computacional

Prévia do material em texto

A lógica computacional é o uso de computadores para estabelecer fatos em um formalismo lógico. Originário das tentativas do século XIX de compreender a natureza do raciocínio matemático, o assunto hoje compreende uma grande variedade de formalismos, técnicas e tecnologias. Uma vertente do trabalho segue a 'abordagem lógica para funções computáveis ​​(LCF)' iniciada por Robin Milner, onde as provas podem ser construídas interativamente ou com a ajuda do código dos usuários (o que não compromete a exatidão). Um refinamento do LCF, chamado Isabelle, mantém essas vantagens ao mesmo tempo em que oferece flexibilidade na escolha do formalismo lógico e automação muito mais forte. A principal aplicação dessas técnicas tem sido provar a correção de sistemas de hardware e software, mas cada vez mais os pesquisadores as aplicam à própria matemática.
Palavras-chave: verificação formal, prova de teoremas, assistentes de prova, Isabelle, lógica para funções computáveis
Vamos para:
1. Introdução
Os computadores controlam tudo, desde marca-passos cardíacos até aeronaves, colocando todos em risco quando falham. Falhas relacionadas ao computador causam regularmente interrupções, danos e, ocasionalmente, morte. Um exemplo recente é o ataque de ransomware WannaCry, que atingiu computadores em todo o mundo, notadamente no Serviço Nacional de Saúde do Reino Unido [ 1 ]. Este ataque foi possibilitado por um defeito específico, o MS17-010, que afetou várias versões do sistema operacional Windows. Em 1994, um erro de divisão de ponto flutuante no processador Pentium forçou a Intel a fazer recall de milhões de chips a um custo de US$ 475 milhões .]. Muitas dessas falhas são causadas por descuido e poderiam ser evitadas pela introdução de métodos de desenvolvimento mais disciplinados. A disciplina final é usar lógica formal e matemática para provar a correção dos projetos. Isso é chamado de verificação formal .
A verificação formal geralmente relaciona uma especificação formal a uma implementação de modelo . Ou seja, começamos com uma descrição completa de todos os serviços a serem entregues pelo sistema (a especificação) e provar que está satisfeito com a implementação do modelo, onde ambos foram expressos em algum formalismo lógico. Uma prova de que todos os serviços serão entregues inclui uma prova de que nenhuma falha ou falha impedirá isso. No entanto, qualquer implementação formalizada deve deixar de fora alguns detalhes da implementação real: por exemplo, a aritmética de precisão finita pode ser considerada exata, a criptografia ser inquebrável ou os componentes de hardware serem infinitamente rápidos. (Os leitores podem se lembrar de problemas de física de livros escolares envolvendo superfícies sem atrito, ou, quando o atrito é incluído, supõe-se que seja linear.) Se o modelo da implementação for muito irreal, as provas sobre ele ignorarão certos modos de falha. Nenhum modelo pode incluir todos os detalhes do mundo real, mas é crucial incluir os aspectos da implementação que mais nos preocupam. Por exemplo, em segurança de computadores, muitos sistemas podem ser quebrados sem derrotar a própria criptografia [3 ]. Então faz sentido supor que a criptografia seja inquebrável se isso simplificar as provas. A validação do modelo é complementar às provas formais e pode envolver uma variedade de métodos, desde julgamento profissional até testes sistemáticos. (É um equívoco pensar que a prova formal elimina a necessidade de testes.)
A verificação formal requer o suporte de software de computador especializado. A lógica computacional está preocupada com a lógica formal implementada em computadores, onde é frequentemente aplicada para resolver problemas relacionados à computação. No entanto, a verificação formal está sendo cada vez mais aplicada a sistemas que interagem com o mundo real e lidam com fenômenos modelados por equações diferenciais, ou que precisam atingir metas expressas em termos de probabilidade. Portanto, tornou-se necessário formalizar o conhecimento matemático.
Vamos para:
2. Uma breve história da lógica formal
Um formalismo lógico é uma linguagem simbólica precisamente definida que inclui primitivos lógicos como 'e' (∧), 'ou' (∨), 'não' (¬), 'implica' (→), 'para todos' (∀) e 'existe' (∃). Pode incluir a capacidade de definir novos símbolos como abreviações de outras expressões. Incluirá regras para fazer deduções lógicas simples: por exemplo, de ϕ ∧ ψ , as conclusões ϕ e ψ podem ser derivadas; de ϕ podemos derivar ϕ ∨ ψ . A partir de tais primitivos básicos, vastas áreas da matemática podem ser derivadas.
A lógica formal emergiu da filosofia no século XIX. A Begriffschrift (linguagem conceitual) de Gottlob Frege foi o primeiro tratamento reconhecivelmente moderno da lógica. Seu trabalho introduziu o projeto de reduzir toda a matemática à lógica [ 4 , 5 ]. Mas o trabalho de Frege terminou com a descoberta do paradoxo de Russell:
Seja R o conjunto de todos os conjuntos que não são membros de si mesmos. Então R é um membro de si mesmo?
Se R é um membro de si mesmo (escrito R ∈ R ) então ele não pode ser um membro de R , e portanto R ∉ R ; por outro lado, se R ∉ R então R ∈ R . Obtemos uma contradição de qualquer maneira. Observe que, contanto que nos limitemos ao inglês, o paradoxo de Russell pode se assemelhar a quebra-cabeças divertidos como 'Esta afirmação é falsa', mas, uma vez que usamos uma linguagem formal com regras estritas, estamos em apuros. Para R ∉ R e R ∈ Rsão ambas verdadeiras, a partir das quais todas as outras declarações podem ser provadas usando lógica básica. Existem muitos outros paradoxos [ 6 , p. 60], por exemplo Burali-Forti, que envolve a construção do maior número ordinal Ω , mas então Ω +1 < Ω . Como observa Gödel,
Ao analisar os paradoxos aos quais a teoria dos conjuntos de Cantor havia levado, [Russell] os libertou de todos os tecnicismos matemáticos, trazendo assim à luz o fato surpreendente de que nossas intuições lógicas (isto é, intuições relativas a noções como verdade, conceito, ser, classe) são autoconscientes. -contraditório. [ 5 , pág. 452]
A partir desse momento, o desenvolvimento da lógica formal foi determinado pela abordagem adotada para resolver os paradoxos. Compreensão de conjuntos — a ideia de que toda propriedade ϕ cria um conjunto, { x | ϕ ( x )} — de alguma forma teve que ser restringido para negar a existência de { x | x ∉ x }, o conjunto de Russell. Uma abordagem foi restringir a compreensão a algum conjunto já existente , digamos A , produzindo o conjunto menor { x ∈ A | ϕ ( x )}: os elementos de A satisfazendo a propriedade ϕ. O universo dos conjuntos não é em si um conjunto, e é construído a partir do conjunto vazio usando algumas primitivas como union e powerset. Essa abordagem leva à moderna teoria axiomática dos conjuntos [ 7 , 8 ].
Outra solução para os paradoxos envolve a noção de tipos . A concepção original de tipo de Whitehead e Russell [ 6 , p. 37] era bastante obscuro [ 5 ], mas em 1940 Church [ 9 ] havia desenvolvido tipos para uma forma que sobrevive até hoje. Em vez de postular uma coleção universal de tudo o que existe, os objetos matemáticos são classificados em tipos distintos, representando coleções menores. Cada construção tem um tipo fixo. Ao formar um conjunto, todos os elementos devem ter o mesmo tipo, digamos τ , e o próprio conjunto terá um tipo diferente, que podemos escrever como conjunto τ  . Assim, a proposição fatal R ∈ Rnão pode nem mesmo ser escrito, porque se R tem o tipo τ , então ele não pode ter o tipo τ  definido ao mesmo tempo.
Os tipos parecem ser impopulares entre os matemáticos, e é comum afirmar que a matemática se baseia na teoria dos conjuntos. Whitehead & Russell [ 6 ] não forneceram notação ou símbolos para os tipos, tornando-os invisíveis, enquanto Church [ 9 ] tinha um único tipo ιde indivíduos englobando todos os objetos que não eram conjuntos nem funções. No entanto, as ideias de Church entraram na ciência da computação, particularmente por meio de sua colaboração com Alan Turing, e no início da década de1960 a noção lógica de tipo estava começando a se confundir com recursos de linguagem de programação (anteriormente chamados de 'modos') que distinguem entre números inteiros e flutuantes. aritmética pontual, por exemplo. A onipresença e a utilidade dos tipos na programação de computadores pode ser uma das razões pelas quais os cientistas da computação tendem a preferir formalismos elaborados.
Ainda outra solução para os paradoxos foi a filosofia da matemática construtiva ou intuicionismo [ 10 ]. Resumidamente, esta é a visão de que objetos matemáticos existem apenas em nossa imaginação, em contraste com a visão platônica ou realista de que objetos matemáticos têm sua própria realidade [ 11 , p. 323]. O intuicionismo exigia um novo tratamento da lógica, em que a disjunção ψ ∨ ϕ só poderia ser verdadeira se soubéssemos qual das duas afirmações, ψ ou ϕ , era verdadeira. Muitas das tautologias básicas da lógica booleana devem então ser rejeitadas, começando com ψ ∨¬ ψ(como não temos uma maneira geral de saber qual alternativa vale) e com ¬¬ ϕ uma afirmação mais fraca que ϕ . No nível dos quantificadores, ∃ x  ϕ ( x ) só poderia ser verdadeiro se conhecêssemos algum valor específico a para o qual ϕ ( a ) valesse. Por essa razão, ∃ x  ϕ ( x ) era uma afirmação mais forte do que ¬[∀ x  ¬ ϕ ( x )], embora na lógica clássica as duas fórmulas sejam equivalentes.
O intuicionismo não pegou os matemáticos convencionais. No entanto, existem fortes ligações entre lógica intuicionista e computação: o conhecimento mencionado no parágrafo anterior tinha que ser computável. As últimas décadas viram a introdução de formalismos [ 12 , 13 ] que identificam fórmulas intuicionistas com tipos elaborados: todo símbolo lógico tem um equivalente no nível do tipo, e provar uma proposição equivale a exibir um elemento do tipo correspondente. Esses formalismos são altamente expressivos e, normalmente, todas as expressões denotam funções computáveis. E há uma identificação direta entre proposições lógicas e tipos [ 14 ]. Por exemplo, provando a fórmula (∀ x ∈ A )(∃y ∈ B )  ϕ ( x , y ) produz uma função computável f tal que se x ∈ A (isto é, x pertence ao tipo A ) então f ( x ) retorna algum y ∈ B emparelhado com algum tipo de 'evidência' afirmando que a propriedade ϕ ( x , y ) é válida. 1 Então teríamos mostrado que f é do tipo (∏  x  ∈  A )(∑  y  ∈  B ) ϕ ( x ,  y ), que podemos identificar com a fórmula acima. Aqui, ∏ e ∑ são as contrapartes de nível de tipo dos quantificadores ∀ e ∃. Os elementos de (∏  x  ∈  A ) B ( x ) são funções f que mapeiam qualquer dado a ∈ A para algum f ( a )∈ B ( a ), generalizando o tipo de função A → B permitindo que o tipo de resultado dependa de o valor do argumento; da mesma forma, os elementos de (∑  x  ∈  A ) B (x ) são pares 〈a , b〉 onde a ∈ A e b ∈ B ( a ), generalizando o produto cartesiano A × B . Esse paradigma de 'proposições como tipos' é o foco de muitas pesquisas atuais; ver Wadler [ 15 ] para uma introdução histórica detalhada.
A verificação formal hoje pode, portanto, ser feita dentro de uma ampla variedade de formalismos lógicos, que incluem
· (i) aquelas baseadas na teoria axiomática dos conjuntos, e sem conceito de tipo;
· (ii) a teoria de tipos simples de Church, onde alguns tipos primitivos podem ser combinados usando operadores como × (produto cartesiano), + (soma disjunta), → (espaço de função) e o construtor de tipo-conjunto mencionado acima;
· (iii)  teorias de tipos dependentes onde os tipos podem receber parâmetros, como em B ( x ), e com vinculação de variáveis ​​como em (∏  x  ∈  A )  B ( x ), permitindo assim o tipo de matrizes n × n, por exemplo .
As abordagens tipadas têm recebido mais atenção em lógica computacional, e abaixo nos concentraremos na teoria simples dos tipos. A terceira abordagem também é o foco de muitas pesquisas.
Existem muitos outros formalismos (por exemplo, lógica modal e de relevância) e técnicas de lógica computacional [ 16 ] não cobertas abaixo. Em particular, técnicas de verificação de modelos [ 17 ] são amplamente utilizadas. Eles podem verificar automaticamente as propriedades do sistema expressas em lógicas temporais (para raciocinar sobre o tempo). No entanto, eles dependem da enumeração do estado em vez da construção de provas, portanto, estão fora do escopo aqui.
Vamos para:
3. Lógica mecanizada: a tradição LCF
Se quisermos provar teoremas em uma lógica formal, o poder do computador é necessário. O desenvolvimento da lógica básica, classes e relações de Whitehead e Russell só atinge (um precursor de!) 1+1=2 depois de centenas de páginas [ 6 , p. 360]. Mathias [ 18 ] apontou que a representação do número 1 como definido por Bourbaki se expande para 4.523.659.424.929 símbolos. Melhores escolhas podem mitigar esses problemas, mas o fato é que as provas formais são extremamente longas e detalhadas.
Idealmente, gostaríamos que o computador provasse nossos teoremas automaticamente. Se isso for impossível, gostaríamos de dar apenas conselhos estratégicos e deixar a máquina trabalhar nos detalhes. Como regra geral, uma maior automação exige a escolha de um formalismo menos expressivo. A lógica booleana (onde temos apenas e, ou, não) é decidível, então, em princípio, todas as questões podem ser resolvidas automaticamente. O problema é conhecido como SAT (para Boolean SATisfiability) e embora uma solução geral seja considerada exponencial no número de variáveis ​​booleanas, existem abordagens heurísticas altamente eficientes. Em uma demonstração dramática dessa tecnologia, Heule & Kullmann [ 19 ] resolveram o problema das triplas de Pitágoras Booleanas, um problema aberto na teoria de Ramsey, gerando uma prova de 200 TB.
Nossa lógica se torna mais expressiva se introduzirmos os quantificadores 'para todos' e 'existe'. Se proibirmos a quantificação sobre funções e conjuntos, isso é chamado de lógica de primeira ordem . Esta teoria está completa : todos os teoremas podem ser provados, com recursos ilimitados. Mas não há uma maneira geral de determinar quanto esforço pode ser necessário ou se a afirmação é falsa. A prova automática de teoremas em lógica de primeira ordem é um campo significativo por si só; uma de suas principais conquistas, embora há 20 anos, é a solução da conjectura de Robbins [ 20 ]. Aliás, dois primeiros titãs da lógica computacional - Hilary Putnam [ 21 ] e Alan Robinson [ 22 ]] — foram treinados como filósofos, e Putnam é lembrado principalmente por seus ensaios.
Infelizmente, a prova de teoremas totalmente automática não pode atender às necessidades de verificação. Aritmética, funções e conjuntos são necessários para especificar até mesmo sistemas simples. Nenhum procedimento automático pode decidir declarações arbitrárias envolvendo aritmética inteira: este é o famoso Entscheidungsproblem de Hilbert , que foi resolvido por Turing [ 23 ]. Outra razão é que as especificações podem se estender a centenas de páginas, e a prova de teoremas totalmente automática não é bem dimensionada. Métodos interativos são a única maneira viável de provar teoremas com base em grandes especificações. 2 E o nome mais associado à prova interativa de teoremas é Robin Milner (FRS 1988).
Milner estava interessado em um formalismo obscuro chamado lógica para funções computáveis ​​(LCF), e construiu um verificador de provas simples enquanto estava na Universidade de Stanford, CA, EUA. Ele tinha duas grandes desvantagens: as provas muitas vezes exigiam longas sequências de passos repetitivos e óbvios e as próprias provas ocupavam muita memória. Ao assumir um cargo na Universidade de Edimburgo, no Reino Unido, ele criou um novo sistema ambicioso chamado Edinburgh LCF [ 24 ], incorporando várias inovações. Uma era fornecer ao usuário uma linguagem de programação especializada, chamada ML (de metalinguagem), para que os usuários pudessem estender o sistema com seu próprio código. Isso permitiria que eles lidassem com qualquer problema de etapas repetitivas codificando sua própria automação. Outra foi eliminar o armazenamento de provas por meio de umatécnica de software conhecida comotipos de dados abstratos . Ao reservar o privilégio de criar teoremas para um pequeno núcleo de código, a necessidade de armazenar provas foi eliminada. A automação fornecida pelo usuário, por mais defeituosa, nunca poderia fazer com que o Edinburgh LCF proclamasse um teorema inválido. O Edinburgh LCF também introduziu toda uma estrutura de técnicas e terminologia:
· —  arquivos de teoria contendo especificações e definições dos conceitos de interesse: as teorias podem se basear em outras teorias, permitindo desenvolvimentos hierárquicos de qualquer tamanho;
· —  prova inversa : começa-se com uma declaração do resultado desejado e reduz-se sucessivamente (usando táticas de prova ) a declarações mais simples até que todas tenham sido provadas;
· —  táticas para combinar táticas de prova de maneira simples, por exemplo, repetição ou execução de uma série de táticas;
· — automação integrada , por exemplo, para simplificar rotinas;
· — juntamente com a capacidade de estender essa automação escrevendo código ML adicional.
Hoje, quase todos os principais provadores de teoremas interativos incorporam essas técnicas e, em muitos casos, código real do LCF de Edimburgo. O ML acabou sendo útil para programação, em geral, e teve um enorme impacto no design de linguagens de programação modernas, como Haskell, OCaml e Scala. Os significados de LCF e ML vão muito além de seus significados literais como siglas. 3
Outra figura significativa na prova interativa de teoremas foi Michael JC Gordon (FRS 1994). Ele criou o sistema HOL [ 25 ], que sobrevive até hoje em várias variantes, incluindo HOL4 e HOL Light [ 26 ]. Todos eles são descendentes do Edinburgh LCF, que ele também ajudou a criar [ 24 ]. Ainda mais significativo é o desenvolvimento de técnicas de Gordon para verificar o hardware do computador; quando ele começou a trabalhar neste tópico no início dos anos 1980, essencialmente todas as pesquisas de verificação eram focadas em software. Gordon desenvolveu técnicas que escalavam de um dispositivo de transistor único para um computador inteiro. Seu principal insight foi que o formalismo correto para essa tarefa era a teoria dos tipos simples , também conhecida como lógica de ordem superior ., daí HOL.
A escolha do HOL foi radical na época. A lógica de primeira ordem era dominante, talvez graças às suas fortes propriedades teóricas, como completude. Gordon observou que tais propriedades eram irrelevantes para verificação e reconheceu que a expressividade adicional de HOL era necessária [ 27 ]. Sua escolha representou um retorno às lógicas mais fortes do início do século XX. Com seus alunos, Gordon estendeu suas técnicas para cobrir uma variedade de sistemas digitais, incluindo hardware de ponto flutuante, algoritmos probabilísticos e muitas outras aplicações. Típico deles é o de Harrison [ 28] verificação de um algoritmo de ponto flutuante para o cálculo da função exponencial. A prova exigiu uma formalização completa do padrão de ponto flutuante do Institute of Electrical and Electronics Engineers (IEEE), em toda a sua complexidade, bem como a análise de erros para o próprio algoritmo.
Enquanto estivermos no tópico de escolhas radicais, não devemos negligenciar a pesquisa em teorias do tipo construtivo. Inspirados originalmente no trabalho de Martin-Löf [ 14 ] e de Coquand & Huet [ 12 ], os pesquisadores construíram uma série de provadores de teoremas interativos, todos seguindo o paradigma LCF de Edimburgo. Por razões de espaço, mencionarei apenas Coq [ 29 ], que se tornou talvez o provador de teoremas interativo mais popular do mundo. Típico de todas essas abordagens é que, por meio de tipos dependentes, o sistema de tipos realiza grande parte da carga de raciocínio que, de outra forma, seria feita por etapas de prova explícitas. Entre as conquistas marcantes realizadas usando Coq estão a verificação formal de um compilador C [ 30] e a formalização do teorema da ordem ímpar [ 31 ]. Um tratamento completo desta linha de trabalho exigiria um artigo separado.
Vamos para:
4. Uma nova arquitetura de prova de teoremas: Isabelle
Durante a década de 1980, muitos formalismos lógicos diferentes competiam pela atenção dos pesquisadores. Além do LCF, as teorias de tipos estavam evoluindo rapidamente, juntamente com uma ampla variedade de formalismos para provar que o software estava correto. Uma desvantagem da abordagem LCF era sua exigência de que cada regra de inferência primitiva tivesse que ser implementada como código de programa e, em seguida, uma segunda vez como uma tática de prova. Um erro no último código poderia impedir o usuário de obter o teorema que pensava ter provado, enquanto um erro no código anterior poderia permitir que o sistema asseverasse declarações falsas como verdadeiras.
Para entender essa desvantagem com mais detalhes, considere uma das regras de inferência lógica mais simples: se ϕ e ψ são teoremas, então sua conjunção também é, ϕ ∧ ψ . Muitas vezes é escrito como
ϕψϕ ∧ ψ .
No entanto, observe que as provas matemáticas frequentemente envolvem suposições temporárias, como quando consideramos os dois casos de algum inteiro n ser par ou ímpar. Cada um dos dois casos é provado com a ajuda da suposição correspondente sobre n . Assim, as pessoas geralmente adotam o chamado cálculo de dedução natural , onde todo raciocínio ocorre dentro de um contexto : um conjunto de fórmulas θ 1 ,…, θ n temporariamente assumidas como verdadeiras. 4 Para minimizar a necessidade de subscritos, normalmente usamos as letras gregas grandes Γe Δ para representar contextos. Se optarmos por tornar isso explícito, nossa regra de inferência pode ser escrita (formando o que é conhecido como cálculo sequencial )
Γ⟹ ϕΔ ⟹ ψΓ, Δ ⟹ ϕ ∧ ψ .
Observe que os dois contextos são combinados quando formamos a conclusão, pois ela depende de tudo que é assumido pelas premissas. E este é o exemplo mais simples possível. Uma série de regras modificam contextos 'descarregando' suposições. O tratamento de variáveis ​​quantificadas introduz outros aspectos técnicos.
Para implementar essa regra usando a arquitetura LCF (que também é adotada pela família HOL e Coq), começamos projetando estruturas de dados que podem representar toda a sintaxe do nosso formalismo. Em seguida, coletamos todas as regras de inferência que precisam ser implementadas; juntos, eles definirão o tipo de dado abstrato thm, o tipo de teoremas. Cada regra terá a forma de uma função codificada em ML. A função para a regra acima terá como argumentos as duas premissas, a saber Γ ⇒ ϕ e Δ⇒ ψ . Essa regra é simples, mas, em outros casos, o código deve fazer verificações sintáticas nas premissas para garantir que elas tenham a forma correta e, se não, sinalizar um erro. Finalmente, a função retorna Γ ,Δ⇒ ϕ ∧ψ como um valor do tipo thm, certificando assim que é um teorema. Essa função específica é chamada CONJno LCF e seus descendentes.
Definir tipo thmconforme descrito acima implementa uma lógica no ML, mas um sistema utilizável também deve suportar a prova inversa: a capacidade de provar uma declaração da forma ϕ ∧ ψ provando as duas partes separadamente. Portanto, precisamos escrever outra função, chamada tactic , que essencialmente executa a regra de inferência ao contrário. Dado o objetivo da forma Γ ⇒ ϕ ∧ ψ , ela retorna os dois subobjetivos separados Γ ⇒ ϕ e Γ ⇒ ψ (e observe que aqui temos um único contexto, Γ , já que estamos trabalhando para trás).
Esses subobjetivos não são teoremas, mas apenas declarações para trabalhar a seguir. Para produzir um teorema no final, a tática também precisa retornar um pedaço de código envolvendo CONJ. Essa função geradora de teoremas é chamada de validação , e o design permite que a maior parte do código fique fora do tipo de dados abstrato thm, do qual depende a solidez de todo o sistema. Se a tática ou sua validação estiver de alguma forma errada, a solidez do sistema não será comprometida. No entanto, o usuário provavelmente ficará desapontado, fazendo o esforço para provar o teorema, mas nunca obtendoo teorema em si. (Em vez disso, um erro será sinalizado, ou possivelmente algum outro teorema entregue.) A retrospectiva de Gordon [ 33 ] sobre essas técnicas é informativa, assim como uma exposição inicial minha [ 33 ]34 ].
Então vemos que, para implementar qualquer cálculo formal usando a arquitetura LCF, toda regra de inferência deve ser implementada em código duas vezes. Poderia haver dezenas de regras, algumas delas complicadas, e qualquer erro seria prejudicial. Modificar um sistema no estilo LCF para implementar um novo formalismo requer meses de trabalho.
A solução para esses problemas é usar a ideia do LCF de uma maneira diferente. Ao invés de focar nos teoremas do formalismo dado, devemos focar nas implicações contextuais da forma Γ ⇒ ϕ . Em particular, tais implicações podem ser unidas de ponta a ponta, criando árvores de prova. Esta abordagem tem uma série de vantagens, como segue.
· — Os contextos são gerenciados da mesma maneira para cada formalismo que está sendo suportado. Enquanto isso, formalismos que gerenciam o contexto explicitamente ainda podem ser manuseados.
· — A construção incremental de uma árvore de prova pode expressar tanto a prova para frente quanto para trás.
· — Os subobjetivos podem até conter variáveis ​​'espaço reservado' compartilhadas, como pode surgir ao provar algo como ∃ x  ( ϕ ( x )∧ ψ ( x )). Ou seja, podemos tentar provar algo da forma ϕ (−) e se conseguirmos provar ϕ ( f (1)), então o outro subobjetivo se tornará ψ (  f (1)).
Mas a principal vantagem é simplesmente que as regras de inferência agora podem ser escritas como asserções. Por exemplo, a regra da conjunção acima se torna
ϕ ,  ψ  ⟹  ϕ  ∧  ψ .
A regra para eliminar uma disjunção (prova por análise de caso) torna-se
ϕ  ∨  ψ , ( ϕ  ⟹  θ ), ( ψ  ⟹  θ ) ⟹  θ .
A regra para introduzir um quantificador existencial torna-se
ϕ ( a ) ⟹ ∃ x  ϕ ( x ).
Essa arquitetura permite que inferências primitivas de um formalismo sejam inseridas mais ou menos como podem aparecer em um livro didático.
Isabelle é o primeiro provador de teoremas genérico do mundo : projetado para apoiar a inferência lógica, em geral, em oposição a qualquer formalismo único. Isabelle toma algumas ideias do HOL para representar a sintaxe formal e as regras de inferência lógica [ 35 ]. Recursos de notação, como ligação de variável (o i em∑eu ∈ eu teu) e princípios como a indução matemática podem ser expressos diretamente, e a conformidade com as apresentações tradicionais pode ser provada [ 32 ]. Tais sistemas meta-lógicos são conhecidos como frameworks lógicos [ 36 ], o primeiro dos quais foi a linguagem AUTOMATH criada por de Bruijn [ 37 ].
Outro princípio fundamental de Isabelle é fornecer os componentes básicos da busca automática de provas no nível mais baixo. As técnicas de resolução da lógica de primeira ordem já haviam se mostrado promissoras. Parecia certo adotar algumas dessas técnicas para fornecer automação para outros formalismos. A junção de implicações, que é o mecanismo central de inferência de Isabelle, é em si uma forma de resolução. Ao longo dos anos, formas cada vez mais sofisticadas de busca automática de provas foram adicionadas a Isabelle [ 38 ].
Essas ideias resistiram ao teste do tempo? Certamente, Isabelle é o único provador de teoremas interativo amplamente usado baseado em uma estrutura lógica. Enquanto isso, os esforços para explorar o poder da prova de teoremas de resolução finalmente resultaram em uma forte integração das duas tecnologias: a ferramenta Sledgehammer [ 39 ] aplica uma bateria de provadores de teoremas de resolução a um problema. Muitas vezes encontra uma prova com a ajuda de fatos obscuros das extensas bibliotecas de Isabelle. Alguns dos trabalhos mais impressionantes feitos usando Isabelle - desde a verificação de protocolos de segurança [ 40 ] a um kernel de sistema operacional verificado [ 41 ] a teoremas matemáticos formalizados [ 42 , 43 ]]—só foi possível por causa da automação de Isabelle.
Por outro lado, a ideia de provar teoremas genéricos é menos bem sucedida. É verdade que Isabelle tem sido usada para apoiar muitos formalismos [ 35 ], incluindo uma versão da teoria do tipo intuicionista de Martin-Löf, lógica de primeira ordem, teoria dos conjuntos e algumas lógicas modais. Isabelle/ZF desenvolve uma quantidade substancial de teoria dos conjuntos de Zermelo-Fraenkel [ 44 ]. Pode-se argumentar que, mesmo no caso de um único formalismo, o uso de uma estrutura lógica torna a noção de construção de prova mais flexível do que a encontrada em sistemas tradicionais do tipo LCF. No entanto, a facilidade de Isabelle em suportar múltiplos formalismos é pouco utilizada. Sua instanciação mais popular de longe é Isabelle/HOL, que no fundo é mais uma implementação do HOL de Church [ 9]. As teorias do tipo construtivo tendem a ser sintaticamente exigentes, de modo que a comunidade de pesquisa sempre preferiu construir suas próprias ferramentas.
As ideias centrais de Isabelle estavam em vigor em 1989 [ 32 ]. Desde então, o desenvolvimento de Isabelle mudou cada vez mais para a Universidade Técnica de Munique, Alemanha, sob a liderança do Prof. Tobias Nipkow. Das inúmeras contribuições feitas lá, a mais importante é a linguagem de prova estruturada Isar [ 45 ], que embora completamente formal inclui muitas expressões idiomáticas matemáticas e muitas vezes permite provas legíveis e de aparência natural. (Até agora, Isabelle seguiu o LCF ao esperar que os usuários gerassem provas diretamente através da linguagem de programação ML.) Extensões às ideias centrais de Isabelle para suportar HOL também se devem a Nipkow e seus colegas, em particular a noção de classes de tipo [ 46 ].]. Os anos viram uma longa série de refinamentos feitos e estudos de caso realizados. Um exemplo notável é a detecção de contra-exemplo [ 47 ], em que Isabelle pode freqüentemente informar ao usuário que a afirmação em consideração não é um teorema.
Vamos para:
5. Formalizando a matemática
A ideia de realizar matemática por máquina remonta pelo menos até Leibniz, que inventou uma máquina de calcular. O primeiro matemático a realizar adequadamente esse sonho foi de Bruijn [ 37 ], cujo projeto AUTOMATH teve início na década de 1960 e culminou na formalização de uma monografia sobre a construção dos reais [ 48 ]. A abordagem de De Bruijn foi baseada em teorias do tipo dependente de sua própria criação. Por volta da mesma época, Andrzej Trybulec teve a ideia de formalizar a matemática usando uma forma de teoria dos conjuntos tipados; uma quantidade substancial de matemática foi traduzida em seu formalismo Mizar, com um tratamento particularmente elegante de estruturas algébricas [ 49 ].
No entanto, o principal impulso para a matemática formalizada surgiu dos requisitos de verificação, que tem sido uma área prioritária para o financiamento da pesquisa. O trabalho inicial de Harrison [ 28 ] para verificar um algoritmo de ponto flutuante para a função exponencial naturalmente levou à formalização de quantidades crescentes de análise. Para verificar algoritmos probabilísticos (que são controlados por lançamentos virtuais de moedas), Hurd [ 50 ] formalizou algumas teorias de probabilidades, incluindo a teoria da medida e a integração de Lebesgue. Trabalhos recentes nessa direção incluem a formalização abrangente de Hölzl [ 51] de cadeias de Markov, um modelo abstrato de sistemas probabilísticos que possui inúmeras aplicações. Esse trabalho geralmente foi feito usando versões de HOL e Isabelle/HOL, mas algoritmos de ponto flutuante também foram verificados usando Coq [ 52 ].
Com o tempo, surgiu uma competição entre os proponentes de diferentes sistemas de verificação com base em quantos teoremas conhecidos haviam sido formalizados em cada um. Harrison [ 26 ] assumiu a liderança aqui, formalizando inúmeros resultados em seu sistema HOL Light. Estes incluíram grande parte da análise complexa [ 53 ] bem como uma prova do teorema dos números primos [ 54 ] e muitos outros resultados. Mais tarde, Harrison desempenhou um papel importante no esforçopara verificar formalmente a prova de Hales de 1998 [ 55 ] da conjectura de Kepler, um problema de 400 anos sobre o empacotamento ótimo de esferas. Árbitros se opuseram a esta prova por causa de sua dependência de extensos cálculos de computador. Em resposta, Hales et al. [ 56] lançou o projeto Flyspeck para verificar formalmente sua prova. Flyspeck foi finalmente bem sucedido, confirmando e simplificando o argumento de Hales [ 57 ]. Algumas das provas formais foram feitas usando Isabelle [ 58 ].
Esta não foi a primeira vez que um resultado matemático foi formalizado para confirmar uma prova contestada. Em 2004, Gonthier formalizou o teorema das quatro cores dentro de Coq [ 59 ]. A prova de 1976 de Appel e Haken era notória por usar um programa de computador sob medida para verificar quase 2.000 casos. Gonthier usou uma estratégia semelhante, com uma diferença crucial: os casos foram verificados por algoritmos que foram verificados usando Coq.
Outros trabalhos desse tipo diziam respeito a provas que, embora gozassem da plena confiança dos matemáticos, tinham outras questões. Minha própria formalização do segundo teorema da incompletude de Gödel [ 43 ] se enquadra nesta categoria: a maioria das provas publicadas carecem muito de detalhes. A formalização de Fleuriot [ 60 ] de algum material dos Principia de Newton é notável por abarcar o uso de infinitesimais por Newton: Fleuriot justifica formalmente as provas originais por meio de análise não padronizada , que dá uma base rigorosa ao raciocínio infinitesimal. Acima de tudo, temos Gonthier et al. de [ 31] projeto monumental para verificar o teorema da ordem ímpar; a questão aqui é simplesmente o tamanho, pois o teorema foi originalmente provado em um artigo de jornal de 255 páginas.
De um modo geral, o objetivo da matemática formalizada é esclarecer dúvidas, resolver ambiguidades e identificar erros. Os matemáticos cometem erros regularmente, como examinado por Lakatos [ 61 ] em sua história da fórmula do poliedro de Euler; ele aponta que mesmo as definições podem estar erradas. Matemáticos modernos famosos também podem ser falíveis:
Quando os alemães planejavam publicar os artigos completos de Hilbert e presenteá-lo com um conjunto por ocasião de um de seus aniversários posteriores, perceberam que não poderiam publicar os artigos em suas versões originais porque estavam cheios de erros, alguns deles bem sério. Então eles contrataram uma jovem matemática desempregada, Olga Taussky-Todd, para revisar os papéis de Hilbert e corrigir todos os erros. Olga trabalhou por três anos. [ 62 , pág. 201]
Cada vez mais, o ímpeto para formalizar a matemática vem dos próprios matemáticos. O medalhista de Fields, Vladimir Voevodsky, escreveu sobre seu horror ao encontrar erros em seu próprio trabalho:
E quem garantiria que eu não me esquecesse de algo e não cometi um erro, se mesmo os erros em argumentos muito mais simples levam anos para serem descobertos? [ 63 , pág. 8]
A teoria do tipo homotopia de Voevodsky [ 64 ] é uma nova abordagem para a formalização da matemática. Dá à teoria do tipo intuicionista de Martin-Löf uma nova interpretação envolvendo espaços topológicos, onde tipos denotam tipos de homotopia. 5 Além disso, essa interpretação sugere o novo axioma da univalência , que diz que as construções isomórficas podem ser identificadas. Essas ideias geraram entusiasmo generalizado e experimentos estão em andamento usando o assistente de prova Coq.
Na direção oposta, a teoria axiomática dos conjuntos também tem sido usada para formalizar a matemática. Conjuntos e tipos denotam coleções, com uma grande diferença: normalmente uma variável pode ter apenas um tipo, mas pode pertencer a qualquer número de conjuntos. Assim, a teoria dos conjuntos pode oferecer a maior flexibilidade na formalização da matemática. Trabalho de minhas próprias preocupações provando um número de propriedades equivalentes ao axioma da escolha [ 65 ] bem como formalizando a prova de Gödel da consistência relativa do axioma da escolha [ 44 ]. Este trabalho pode ser criticado como sendo apenas sobre a própria teoria dos conjuntos. No entanto, trabalho recente de Zhan [ 66 ] mostra que a teoria dos conjuntos também pode ser usada para formalizar resultados matemáticos tradicionais da teoria dos grupos, topologia de conjuntos de pontos e análise real.
Vamos para:
6. Obstáculos à formalização da matemática
Os obstáculos à formalização da matemática talvez não sejam o que as pessoas imaginam. O teorema de Gödel não é especialmente relevante para a matemática na prática. Mesmo o Entscheidungsproblem não é tão relevante: quando temos procedimentos de decisão, eles podem ser muito caros para serem executados. De qualquer forma, nossa ambição é ajudar os matemáticos, não substituí-los por computadores. Os obstáculos que enfrentamos assumem uma variedade de formas.
(a) Fundacional
A imaginação de um matemático é irrestrita, mas todo cálculo formal é uma estrutura rígida e, em última análise, uma prisão. Por exemplo, a teoria axiomática dos conjuntos começa criando um mundo grande o suficiente para a matemática do século XIX, então o escala através de princípios poderosos para criar um universo inconcebivelmente grande de objetos matemáticos. Ele contém estranhezas como o limite de {ℵ 0 ,ℵ ℵ 0 ,ℵ ℵ ℵ 0 ,…}, um cardinal λ satisfazendo a equação λ=ℵ λ . (A sequência ℵ enumera as cardinalidades infinitas, começando com ℵ 0 : a cardinalidade dos inteiros.) Boolos [ 67] afirma francamente que não pode acreditar que tal objeto exista. E, no entanto, a teoria das categorias [ 68 ] começa criando a categoria de conjuntos e funções, assumindo de uma só vez a existência de um objeto matemático incorporando todo o universo de conjuntos e construindo sobre ele. Então, em um momento nosso universo parece muito grande, e um momento depois ele se tornou muito pequeno.
(b) Conceitual
A intuição desempenha um papel enorme na matemática. Um matemático vê facilmente que uma certa função – talvez definida por uma integral complicada – é contínua. Muitas propriedades de convergência são óbvias. Mas, em alguns casos, as provas formais são enormes [ 54 ]. Há uma variedade de respostas a esta situação. Uma é fornecer automação adicional para lidar com tarefas específicas, como provar propriedades assintóticas [ 69 ]. Outra é aceitar que alguns fatos aparentemente óbvios, como o teorema da curva de Jordan, que afirma que toda curva fechada simples divide o plano em uma região interior e uma região externa, realmente são extremamente difíceis de provar com rigor [ 70 ]. Outra é aceitar que muitas afirmações aparentemente óbvias são, na verdade, falsas .]. Mas, por tudo isso, o uso de qualquer formalismo lógico exige imensa paciência.
(c) Notacional
A linguagem da matemática evoluiu ao longo dos séculos. Pode ser inconsistente e ambíguo – compare sin 2 ⁡ x com y 2 x – mas é familiar e razoavelmente eficaz. Qualquer formalismo implementado em um computador será código e se parecerá com ele. Por exemplo, o teorema fundamental da álgebra afirma que se n é um inteiro positivo e a 0 , a 1 ,…, a n são números complexos com a n ≠0, então a n z n +⋯+ a 1 z + a 0 =0 para algum complexoz . A versão HOL Light relaxa a pré-condição para 0 = 0; caso contrário, os a k não são todos zero para k = 1,…, n :
!a n. a(0) = Cx(&0) \/ ∼(!k. k IN 1..n ==> a(k) = Cx(&0))
      ==> ?z. vsum(0..n) (\i. a(i) * z pow i) = Cx(&0)
A elegância da notação matemática é completamente perdida. Isabelle faz um pouco melhor, permitindo o alfabeto grego e muitos símbolos matemáticos, mas todas essas linguagens ainda são código.
Outra complicação merece menção. Muitas expressões da matemática podem ser indefinidas , por exemplo, alguns limites, derivadas, integrais ou simplesmente x / y quando y =0. Um cálculo formal pode lidar com esse problema de várias maneiras diferentes [ 42 , §5.1]. Assim, podemos descobrir que x / y = x / y (quando x /0 denota algum valor arbitrário) ou que x / y = x / y se e somente se y≠0 (quando consideramos afirmações primitivas sobrevalores indefinidos como necessariamente falsas) ou podemos descobrir que o próprio ato de escrever x / y é proibido, a menos que possamos provar y ≠0. Esta última abordagem pode ser inconveniente [ 71 , §4]; na verdade, cada abordagem tem seus pontos bons e ruins. A ideia de que x / y é sempre algo horroriza alguns matemáticos (especialmente, se formos mais longe, como em Isabelle, e estipularmos que x /0=0). Tratamentos elaborados de definição rendem maior poder expressivo: pagos, como sempre, por notações mais complicadas e provas mais difíceis.
Vamos para:
7. O caminho a seguir
Ao longo deste artigo, reduzimos nosso foco várias vezes, buscando deliberadamente pesquisa em oposição a aplicações. Isso é necessário porque ferramentas de lógica computacional, interpretadas de forma ampla, são hoje amplamente utilizadas no desenvolvimento de hardware, software e na prestação de serviços online. Corremos o risco, talvez, de ignorar a principal motivação da lógica computacional: provar a correção dos sistemas computacionais. Então, vamos tomar um momento para considerar um problema básico em ciência da computação: a correção do compilador.
Um compilador é um software que traduz o código do programa (escrito em uma linguagem de programação como C ou Java) em algum tipo de formato binário que pode ser executado no hardware do computador. Os compiladores são complexos, principalmente porque usam uma ampla variedade de técnicas sofisticadas para gerar código binário que será executado o mais rápido possível. Se o compilador estiver de alguma forma com defeito, ele poderá introduzir erros no código que é realmente executado. As pessoas têm procurado provar que os compiladores estão corretos usando técnicas de lógica computacional [ 30 ]. Mas mesmo se finalmente obtivermos um compilador correto, como o traduzimos em código binário executável? Uma complicação adicional é que a semântica de uma linguagem como C tem pouco em comum com a forma como C é usado em software real, que depende de inúmeros comportamentos indefinidos.
Kumar et ai. [ 72 ] resolveram esse problema do ovo e da galinha. Eles projetaram sua própria linguagem de programação, CakeML, com uma semântica limpa. Eles expressam um algoritmo de compilação simples como uma função matemática no HOL4 (um descendente do sistema HOL original de Gordon). Eles traduzem o mesmo algoritmo para CakeML e o compilam para binário (para a popular arquitetura ×86) usando o próprio HOL4 , dando alta garantia de correção. Isso produz uma versão confiável do compilador em formato binário. Sua abordagem é um exemplo da conhecida técnica de bootstrapping, onde um compilador é construído para uma linguagem simples mas adequada e então usado como uma ferramenta para promover seu próprio desenvolvimento até que a linguagem completa seja suportada. Nesse caso, o processo de bootstrap inclui verificação e é possível porque o HOL4 pode lidar com o código binário completo do compilador CakeML. Este é um representante de um grande corpo de pesquisa preocupado com o tratamento de funções matemáticas definidas dentro de um provador de teoremas como código executável.
Os leitores que quiserem aprofundar esses tópicos encontrarão pesquisas disponíveis sobre matemática formalmente verificada [ 73 ] e sobre a história da prova interativa de teoremas [ 74 , 75 ].
Vamos para:
Reconhecimentos
Angeliki Koutsoukou-Argyraki comentou um rascunho deste artigo. Os árbitros também fizeram comentários perspicazes. Também gostaria de agradecer a Mike Gordon FRS e Robin Milner FRS por sua orientação.
Vamos para:
Notas de rodapé
1 Assim, uma forma do axioma da escolha é realmente demonstrável neste sistema [ 14 , p. 516].
2 Provadores de teoremas interativos também são chamados de assistentes de prova .
3 ML também pode se referir ao aprendizado de máquina.
4 Provas matemáticas também introduzem quantidades temporárias, como quando permitimos que x denote a raiz de algum polinômio. Portanto, os contextos podem incluir uma string de variáveis ​​vinculadas, mas os detalhes [ 32 ] são muito complicados para serem apresentados aqui.
5 Uma homotopia entre duas funções contínuas f e g é uma 'deformação' contínua de f em g . Com este conceito pode-se definir uma relação de equivalência em espaços topológicos, e as classes de equivalência resultantes são chamadas de tipos de homotopia .
Vamos para:
Acessibilidade de dados
Isabelle pode ser baixado em https://isabelle.in.tum.de .
Vamos para:
Interesses competitivos
Declaro que não tenho interesse concorrente.
Vamos para:
Financiamento
Grande parte da pesquisa relatada aqui foi apoiada pelo EPSRC ou seus antecessores, ou por agências de financiamento alemãs e da UE, com mais de 40 anos.
Vamos para:
perfil do autor
Lawrence Paulson FRS é Professor de Lógica Computacional na Universidade de Cambridge, onde ocupou cargos estabelecidos desde 1983. Ele escreveu mais de 100 artigos de conferências e periódicos, bem como quatro livros. Ele introduziu o popular ambiente de prova de teoremas de Isabelle em 1986 e fez contribuições para a verificação de protocolos criptográficos, a formalização da matemática, tecnologia automatizada de prova de teoremas e outros campos. Ele conseguiu uma análise formal do onipresente protocolo TLS, que é usado para garantir compras online, e a verificação formal do segundo teorema da incompletude de Gödel. Em 2008, ele introduziu o MetiTarski, um provador automático de teoremas para funções de valor real, como logaritmos e exponenciais.
Vamos para:
Referências
1. Woollaston V. 2017. WannaCry ransomware: o que é e como se proteger. Consulte http://www.wired.co.uk/article/wannacry-ransomware-virus-patch .
2. Bem TR. 2011. Falha do Pentium FDIV. Consulte http://www.trnicely.net/pentbug/pentbug.html .
3. Lowe G. 1996. Alguns novos ataques aos protocolos de segurança. Em Proc. 9º Workshop de Fundamentos de Segurança de Computadores , pp. 162–169. Silver Spring, MD: IEEE Computer Society Press.
4. Boolos GS. 1998. Gottlob Frege e os fundamentos da aritmética. Em Lógica, lógica e lógica (ed. GS Boolos), pp. 143–154. Cambridge, MA: Harvard University Press.
5. Gödel K. 1983. A lógica matemática de Russell. Em Filosofia da matemática: leituras selecionadas (eds P Benacerraf, H Putnam), 2ª ed., pp. 447–469. Cambridge, Reino Unido: Cambridge University Press.
6. Whitehead AN, Russell B. 1962. Principia mathematica . Cambridge, Reino Unido: Cambridge University Press; Edição em brochura até *56, abreviada a partir da 2ª edição (1927). [ Google Acadêmico ]
7. Boolos GS. 1998. A concepção iterativa de conjunto. Em Lógica, lógica e lógica (ed. GS Boolos), pp. 13–29. Cambridge, MA: Harvard University Press.
8. Kunen K. 1980. Teoria dos conjuntos: uma introdução às provas de independência . Amsterdã, Holanda: Holanda do Norte. [ Google Acadêmico ]
9. Church A. 1940. Uma formulação da teoria simples dos tipos . J. Symb. Lógica 5 , 56-68. ( doi:10.2307/2266170 ) [ Google Scholar ]
10. Heyting A. 1983. Os fundamentos intuicionistas da matemática. Em Filosofia da matemática: leituras selecionadas (eds P Benacerraf, H Putnam), 2ª ed., pp. 52–61. Cambridge, Reino Unido: Cambridge University Press.
11. Gödel K. 1995. Alguns teoremas básicos sobre os fundamentos da matemática e suas implicações. Em Kurt Gödel: obras completas (ed. S Feferman), vol. III, pp. 304-323. Oxford, Reino Unido: Oxford University Press.
12. Coquand T, Huet G. 1988. O cálculo das construções . Inf. Computar. 76 , 95-120. ( doi:10.1016/0890-5401(88)90005-3 ) [ Google Scholar ]
13. Martin-Löf P. 1975. Uma teoria intuicionista dos tipos: parte predicativa. In Logic colloquium '73 (eds H Rose, J Shepherdson). Estudos em Lógica e Fundamentos da Matemática, n. 80, pp. 73-118. Amsterdã, Holanda: Holanda do Norte.
14. Martin-Löf P. 1984. Matemática construtiva e programação de computadores . Fil. Trans. R. Soc. Londres. A 312 , 501-518. ( doi:10.1098/rsta.1984.0073 ) [ Google Scholar ]
15. Wadler P. 2015. Proposições como tipos . Comum. ACM 58 , 75-84. ( doi:10.1145/2699407 ) [ Google Scholar]
16. Huth M, Ryan M. 2004. Lógica em ciência da computação: modelagem e raciocínio sobre sistemas , 2ª ed. Cambridge, Reino Unido: Cambridge University Press. [ Google Acadêmico ]
17. Jhala R, Majumdar R. 2009. Verificação de modelo de software . Computação ACM. Sobreviv. 41 , 21:1–21:54. ( doi: 10.1145/1592434.1592438 ) [ Google Scholar ]
18. Mathias ARD. 2002. Termo de duração 4 523 659 424 929 . Síntese 133 , 75-86. ( doi:10.1023/A:1020827725055 ) [ Google Scholar ]
19. Heule MJH, Kullmann O. 2017. A ciência da força bruta . Comum. ACM 60 , 70-79. ( doi:10.1145/3107239 ) [ Google Scholar ]
20. McCune W. 1997. Solução do problema de Robbins . J. Autom. Raciocínio 19 , 263–276. ( doi:10.1023/A:1005843212881 ) [ Google Scholar ]
21. Davis M, Putnam H. 1960. Um procedimento de computação para a teoria da quantificação . J. ACM 7 , 207-215. ( doi: 10.1145/321033.321034 ) [ Google Scholar ]
22. Robinson JA. 1965. Uma lógica orientada a máquina baseada no princípio de resolução . J. ACM 12 , 23-41. ( doi: 10.1145/321250.321253 ) [ Google Scholar ]
23. Turing AM. 1936. Em números computáveis, com uma aplicação ao Entscheidungsproblem . Proc. Londres. Matemática. Soc. 2 , 230-265. ( doi:10.1112/plms/s2-42.1.230 ) [ Google Scholar ]
24. Gordon MJC, Milner R, Wadsworth CP. 1979. Edimburgo LCF: uma lógica mecanizada de computação . Notas de aula em Ciência da Computação, no. 78. Berlim, Alemanha: Springer.
25. Gordon MJC, Melham TF. 1993. Introdução ao HOL: um ambiente de prova de teoremas para lógica de ordem superior . Cambridge, Reino Unido: Cambridge University Press. [ Google Acadêmico ]
26. Harrison J. 1996. HOL Light: uma introdução tutorial. Em métodos formais em desenho assistido por computador: FMCAD '96 (eds MK Srivas, AJ Camilleri). Notas de aula em Ciência da Computação, vol. 1166, pp. 265-269. Berlim, Alemanha: Springer.
27. Gordon MJC. 1986. Por que a lógica de ordem superior é um bom formalismo para especificar e verificar hardware. Em aspectos formais do projeto VLSI (eds G Milne, PA Subrahmanyam), pp. 153-177. Amsterdã, Holanda: Holanda do Norte.
28. Harrison J. 2000. Verificação de ponto flutuante em HOL Light: a função exponencial . Forma. Métodos. Sistema Des. 16 , 271-305. ( doi:10.1023/A:1008712907154 ) [ Google Scholar ]
29. Bertot Y, Castéran P. 2004. Prova interativa de teoremas e desenvolvimento de programas. Coq'Art: o cálculo das construções indutivas . Berlim, Alemanha: Springer. [ Google Acadêmico ]
30. Leroy X. 2006. Certificação formal de back-end de compilador ou: programação de compilador com assistente de prova. In POPL '06: Registro da Conferência do 33º Simpósio ACM SIGPLAN-SIGACT sobre Princípios de Linguagens de Programação, Nova York, NY, EUA , pp. 42–54. Nova York, NY: ACM Press.
31. Gonthier G. et al. 2013. Uma prova verificada por máquina do teorema da ordem ímpar. Na prova interativa de teoremas (eds S Blazy, C Paulin-Mohring, D Pichardie). Notas de aula em Ciência da Computação, vol. 7998, pp. 163-179. Berlim, Alemanha: Springer.
32. Paulson LC. 1989. A fundação de um provador de teorema genérico . J. Autom. Raciocínio 5 , 363-397. ( doi:10.1007/BF00248324 ) [ Google Scholar ]
33. Gordon MJC. 2015. Táticas para raciocínio mecanizado: um comentário sobre Milner (1984) 'o uso de máquinas para auxiliar na prova rigorosa' . Fil. Trans. R. Soc. A 373 , 20140234 ( doi:10.1098/rsta.2014.0234 ) [ PMC free article ] [ PubMed ] [ Google Scholar ]
34. Paulson LC. 1986. Dedução natural como resolução de ordem superior . J. Programa Lógico. 3 , 237-258. ( doi:10.1016/0743-1066(86)90015-4 ) [ Google Scholar ]
35. Paulson LC. 1990. Isabelle: os próximos 700 provadores de teoremas. Em lógica e ciência da computação (ed. P Odifreddi), pp. 361-386. Nova York, NY: Academic Press.
36. Harper R, Honsell F, Plotkin G. 1993. Uma estrutura para definir lógicas . J. ACM 40 , 143-184. ( doi: 10.1145/138027.138060 ) [ Google Scholar ]
37. de Bruijn NG. 1980. Levantamento do projeto AUTOMATH. Em To HB Curry: ensaios em lógica combinatória, cálculo lambda e formalismo (eds J Seldin, J Hindley), pp. 579-606. Nova York, NY: Academic Press.
38. Paulson LC. 1999. Um provador de tableau genérico e sua integração com Isabelle . J. Univers. Computar. Sci. 5 , 73-87. ( doi:10.3217/jucs-005-03-0073 ) [ Google Scholar ]
39. Paulson LC, Blanchette JC. 2010. Três anos de experiência com marreta, uma ligação prática entre provadores de teoremas automáticos e interativos. Em Proc. 8ª Int. Workshop sobre a Implementação de Lógicas, IWIL 2010, Yogyakarta, Indonésia, 9 de outubro de 2011 (eds G Sutcliffe, S Schulz, E Ternovska). Série EPiC em Computação, vol. 2, pp. 1–11. Manchester, Reino Unido: EasyChair.
40. Paulson LC. 1999. Análise indutiva do protocolo de Internet TLS . ACM Trans. Inf. Sistema Seguro. 2 , 332-351. ( doi: 10.1145/322510.322530 ) [ Google Scholar ]
41. Klein G. 2010. sel4: verificação formal de um kernel de sistema operacional . Comum. ACM 53 , 107-115. ( doi: 10.1145/1629575.1629596 ) [ Google Scholar ]
42. Avigad J, Hölzl J, Serafin L. 2017. Uma prova formalmente verificada do teorema do limite central . J. Autom. Raciocínio 59 , 389–423. ( doi:10.1007/s10817-017-9404-x ) [ Google Scholar ]
43. Paulson LC. 2014. Uma prova assistida por máquina de teoremas de incompletude de Gödel para a teoria de conjuntos hereditariamente finitos . Rev. Symb. Registro. 7 , 484-498. ( doi:10.1017/S1755020314000112 ) [ Google Scholar ]
44. Paulson LC. 2003. A consistência relativa do axioma da escolha – mecanizado usando Isabelle/ZF . LMS J. Comput. Matemática. 6 , 198-248. Veja http://www.lms.ac.uk/jcm/6/lms2003-001/ ( doi:10.1112/S1461157000000449 ) [ Google Scholar ]
45. Wenzel M. 2007. Isabelle/Isar—uma estrutura genérica para documentos de prova legíveis por humanos . Viga. Registro. Gram. Retor. 10 , 277-297. [ Google Acadêmico ]
46. ​​Wenzel M. 1997. Classes de tipos e sobrecarga em lógica de ordem superior. Em Teorema provando em lógicas de ordem superior: TPHOLs '97 (eds EL Gunter, A Felty). Notas de aula em Ciência da Computação, vol. 1275, pp. 307-322. Berlim, Alemanha: Springer.
47. Blanchette JC, Nipkow T. 2010. Nitpick: um gerador de contra-exemplo para lógica de ordem superior baseado em um localizador de modelo relacional. Na prova interativa de teoremas (eds M Kaufmann, LC Paulson). Notas de aula em Ciência da Computação, vol. 6172, pp. 131-146. Berlim, Alemanha: Springer.
48. Jutting L. 1977. Verificando o 'Grundlagen' de Landau no sistema AUTOMATH. Tese de doutorado, Eindhoven University of Technology, Eindhoven, Holanda.
49. Rudnicki P, Schwarzweller C, Trybulec A. 2001. Álgebra comutativa no sistema Mizar . J. Symb. Computar. 32 , 143-169. ( doi:10.1006/jsco.2001.0456 ) [ Google Scholar ]
50. Hurd J. 2002. Verificação do teste de primalidade probabilística de Miller-Rabin . J. Lógica Álgebr. Programa. 56 , 3-21. ( doi:10.1016/S1567-8326(02)00065-6 ) [ Google Scholar ]
51. Hölzl J. 2017. Cadeias de Markov e processos de decisão de Markov em Isabelle/HOL . J. Autom. Raciocínio 59 , 345–387. ( doi:10.1007/s10817-016-9401-5 ) [ Google Scholar ]
52. Boldo S, Joldes M, Muller J, Popescu V. 2017. Verificação formal de um algoritmo de renormalização de expansão de ponto flutuante. Em Proc. de Prova Interativa de Teoremas - 8º Int. Conf., ITP 2017, Brasília, Brasil, 26–29 de setembro de 2017 (eds M Ayala-Rincón, CA Muñoz), pp. 98–113. Berlim, Alemanha: Springer International Publishing.
53. Harrison J. 2007. Formalizando a análise complexa básica . Viga. Registro. Gram. Retor. 10 , 151-165. [ Google Acadêmico ]
54. Harrison J. 2009. Formalizando uma prova analítica do teorema dos números primos . J. Autom. Raciocínio 43 , 243-261. ( doi:10.1007/s10817-009-9145-6 ) [ Google Scholar ]
55. Hales TC.1998. Uma visão geral da conjectura de Kepler. ( http://arxiv.org/abs/math/9811071 . )
56. Hales TC. et ai. 2015Uma prova formal da conjectura de Kepler. ( http://arxiv.org/abs/1501.02155 )
57. Hales TC, Harrison J, McLaughlin S, Nipkow T, Obua S, Zumkeller R. 2010. Uma revisão da prova da conjecturade Kepler . Computação Discreta. Geom. 44 , 1-34. ( doi:10.1007/s00454-009-9148-4 ) [ Google Scholar ]
58. Nipkow T, Bauer G, Schultz P. 2006. Flyspeck I: gráficos mansos. Em Proc. de Raciocínio Automatizado, Terceira Conferência Conjunta Internacional, IJCAR 2006, Seattle, WA, 17–20 de agosto de 2006 (eds U Furbach, N Shankar). Notas de Palestra em Inteligência Artificial, vol. 4130, pp. 21-35. Berlim, Alemanha: Springer.
59. Gonthier G. 2008. O teorema das quatro cores: engenharia de uma prova formal. Em matemática de computador (ed. D Kapur). Notas de Palestra em Ciência da Computação, vol. 5081, pp. 333-333. Berlim, Alemanha: Springer.
60. Fleuriot JD. 2001. Uma combinação de prova de teoremas de geometria e análise não padronizada, com aplicação aos Principia de Newton . Berlim, Alemanha: Springer. [ Google Acadêmico ]
61. Lakatos I. 1976. Provas e refutações: a lógica da descoberta matemática . Cambridge, Reino Unido: Cambridge University Press. [ Google Acadêmico ]
62. Rota GC. 2009. Pensamentos indiscretos . Berlim, Alemanha: Springer. [ Google Acadêmico ]
63. Voevodsky V. 2014. As origens e motivações das fundações univalentes. In The Institute Letter , pp. 8–9. Princeton, NJ: Instituto de Estudos Avançados. Consulte https://www.ias.edu/ideas/2014/voevodsky-origins .
64. O Programa de Fundações Univalentes. 2013. Teoria do tipo homotopia: fundamentos univalentes da matemática. Consulte https://homotopytypetheory.org/book .
65. Paulson LC, Grabczewski K. 1996. Mecanização da teoria dos conjuntos: aritmética cardinal e o axioma da escolha . J. Autom. Raciocínio 17 , 291–323. ( doi:10.1007/BF00283132 ) [ Google Scholar ]
66. Zhan B. 2017. Formalização do grupo fundamental em teoria dos conjuntos não tipados usando Auto2. Em Proc. de Prova Interativa de Teoremas - 8º Int. Conf., ITP 2017, Brasília, Brasil, 26–29 de setembro de 2017 (eds M Ayala-Rincón, CA Muñoz), pp. 514–530. Berlim, Alemanha: Springer International Publishing.
67. Boolos GS. 1998. Devemos acreditar na teoria dos conjuntos? Em Lógica, lógica e lógica (ed. GS Boolos), pp. 120–132. Cambridge, MA: Harvard University Press.
68. MacLane S. 1971. Categorias para o matemático de trabalho . Berlim, Alemanha: Springer. [ Google Acadêmico ]
69. Eberl M. 2017. Assintótica semiautomática em Isabelle/HOL. Consulte https://www.newton.ac.uk/seminar/20170705133014302 .
70. Hales TC. 2007. O teorema da curva de Jordan, formalmente e informalmente . Sou. Matemática. Seg. 114 , 882-894. ( doi: 10.1080/00029890.2007.11920481 ) [ Google Scholar ]
71. Boldo S, Lelay C, Melquiond G. 2015. Coquelicot: uma biblioteca amigável de análise real para Coq . Matemática. Computar. Sci. 9 , 41-62. ( doi:10.1007/s11786-014-0181-1 ) [ Google Scholar ]
72. Kumar R, Myreen MO, Norrish M, Owens S. 2014. CakeML: uma implementação verificada de ML. Em Proc. Simpósio ACM SIGPLAN-SIGACT sobre Princípios de Linguagens de Programação, POPL '14 , pp. 179–191. Nova York, NY: ACM.
73. Avigad J, Harrison J. 2014. Matemática formalmente verificada . Comum. ACM 57 , 66-75. ( doi:10.1145/2591012 ) [ Google Scholar ]
74. Geuvers H. 2009. Assistentes de prova: história, ideias e futuro . Sadhana 34 , 3-25. ( doi:10.1007/s12046-009-0001-5 ) [ Google Scholar ]
75. Harrison J, Urban J, Wiedijk F. 2014. História da prova interativa de teoremas. No Manual da história da lógica (lógica computacional) (ed. J Siekmann), vol. 9, pp. 135-214. Amsterdã, Holanda: Elsevier.
Artigos de Anais. Ciências Matemáticas, Físicas e de Engenharia são fornecidas aqui, cortesia da Royal Society
OUTROS FORMATOS
· PubReader
 
· PDF (388K)
AÇÕES
· Citar
· Favoritos
COMPARTILHAR
·  
 
·  
 
·  
RECURSOS
· Artigos semelhantes
· Citado por outros artigos
· Links para bancos de dados NCBI
                                            
SIGA O NCBI
Conecte-se com NLM
· 
 
· 
 
· 
Biblioteca Nacional de Medicina
8600 Rockville Pike
Bethesda, MD 20894
Políticas da Web Divulgação de Vulnerabilidade
FOIA
HHS
Ajuda Carreiras em
Acessibilidade
· NLM
· NIH
· HHS
· USA.gov
https://ww
 
 
 
 
 
 
 
 
 
NLM